Prove B1 and B3, and make the TLA+ model terminate#3

orange-dot merged 2 commits into

mainorange-dot/ekk-runtime:mainfrom

b2-evaluate-ballot-prooforange-dot/ekk-runtime:b2-evaluate-ballot-proofCopy head branch name to clipboard