Proof Status: THEOREM L

▶ <1>5 <1>5. TypeOK /\ H_OnePrimaryPerTerm /\ CommitEntryAction => H_OnePrimaryPerTerm' BY DEF TypeOK,CommitEntryAction,CommitEntry,H_OnePrimaryPerTerm 9/9 tlapm

#54 L176:38:176:40 proved smt

#55 L176:41:176:45 trivial tlapm

#56 L176:47:176:51 trivial tlapm

#57 L176:53:176:57 trivial tlapm

#58 L177:42:177:44 proved smt

#59 L177:45:177:49 trivial tlapm

#60 L177:51:177:55 trivial tlapm

#61 L177:57:177:61 trivial tlapm

#62 L177:63:177:67 trivial tlapm

▶ <1>6 <1>6. TypeOK /\ H_OnePrimaryPerTerm /\ UpdateTermsAction => H_OnePrimaryPerTerm' 128/128 tlapm

#49 L182:19:182:21 proved smt 1.3s (27%)

#50 L182:22:182:26 trivial tlapm

#51 L182:28:182:32 trivial tlapm

#52 L182:34:182:38 trivial tlapm

#53 L182:40:182:44 trivial tlapm

#63 L179:15:179:17 proved smt

#64 L179:18:179:22 trivial tlapm

#65 L179:24:179:28 trivial tlapm

#66 L179:30:179:34 trivial tlapm

#67 L181:15:181:17 proved smt

#68 L181:18:181:22 trivial tlapm

▶ <2>1 <2>1. currentTerm[i] > currentTerm[j] 18/18 tlapm

#75 L185:50:185:52 proved smt

#76 L185:53:185:57 trivial tlapm

#77 L185:59:185:63 trivial tlapm

#78 L185:65:185:69 trivial tlapm

#79 L186:54:186:56 proved smt

#80 L186:57:186:61 trivial tlapm

#81 L186:63:186:67 trivial tlapm

#82 L186:69:186:73 trivial tlapm

#83 L186:75:186:79 trivial tlapm

#116 L225:48:225:50 proved smt

#117 L225:51:225:55 trivial tlapm

#124 L229:49:229:51 proved smt

#125 L229:52:229:56 trivial tlapm

#126 L229:58:229:62 trivial tlapm

#127 L229:64:229:68 trivial tlapm

#128 L230:33:230:35 proved smt

#129 L230:36:230:40 trivial tlapm

#130 L230:42:230:46 trivial tlapm

▶ <2>2 <2>2. currentTerm' = [currentTerm EXCEPT ![j] = currentTerm[i]] 10/10 tlapm

#84 L188:15:188:17 proved smt

#85 L188:18:188:22 trivial tlapm

#97 L197:44:197:46 proved smt

#98 L197:47:197:51 trivial tlapm

#99 L199:13:199:15 proved smt

#100 L199:16:199:20 trivial tlapm

#101 L199:22:199:26 trivial tlapm

#102 L199:28:199:32 trivial tlapm

#103 L199:34:199:38 trivial tlapm

#104 L199:40:199:44 trivial tlapm

▶ <2>3 <2>3. state' = [state EXCEPT ![j] = Secondary] 11/11 tlapm

#69 L195:19:195:21 proved smt 1.1s (21%)

#70 L195:22:195:26 trivial tlapm

#71 L195:28:195:32 trivial tlapm

#72 L195:34:195:38 trivial tlapm

#73 L195:40:195:44 trivial tlapm

#74 L195:46:195:50 trivial tlapm

#86 L190:15:190:17 proved smt

#87 L190:18:190:22 trivial tlapm

#88 L190:24:190:28 trivial tlapm

#89 L190:30:190:34 trivial tlapm

#115 L224:11:224:13 proved smt

▶ <2>4 <2>4. state[s1] = Primary /\ s1 # j 2/2 smt

#90 L192:15:192:17 proved smt

#91 L192:18:192:22 trivial tlapm

▶ <2>3 BY <2>3 DEF TypeOK 11/11 tlapm

#69 L195:19:195:21 proved smt 1.1s (21%)

#70 L195:22:195:26 trivial tlapm

#71 L195:28:195:32 trivial tlapm

#72 L195:34:195:38 trivial tlapm

#73 L195:40:195:44 trivial tlapm

#74 L195:46:195:50 trivial tlapm

#86 L190:15:190:17 proved smt

#87 L190:18:190:22 trivial tlapm

#88 L190:24:190:28 trivial tlapm

#89 L190:30:190:34 trivial tlapm

#115 L224:11:224:13 proved smt

▶ <2>5 <2>5. state[t1] = Primary /\ t1 # j 6/6 tlapm

#92 L194:15:194:17 proved smt

#93 L194:18:194:22 trivial tlapm

#120 L228:55:228:57 proved smt

#121 L228:58:228:62 trivial tlapm

#122 L228:64:228:68 trivial tlapm

#123 L228:70:228:74 trivial tlapm

▶ <2>3 BY <2>3 DEF TypeOK 11/11 tlapm

#69 L195:19:195:21 proved smt 1.1s (21%)

#70 L195:22:195:26 trivial tlapm

#71 L195:28:195:32 trivial tlapm

#72 L195:34:195:38 trivial tlapm

#73 L195:40:195:44 trivial tlapm

#74 L195:46:195:50 trivial tlapm

#86 L190:15:190:17 proved smt

#87 L190:18:190:22 trivial tlapm

#88 L190:24:190:28 trivial tlapm

#89 L190:30:190:34 trivial tlapm

#115 L224:11:224:13 proved smt

▶ <2>6 <2>6. currentTerm'[s1] = currentTerm[s1] 6/6 tlapm

#17 L201:16:201:18 proved smt

#18 L201:19:201:23 trivial tlapm

#19 L201:25:201:29 trivial tlapm

#94 L196:46:196:48 proved smt

#95 L196:49:196:53 trivial tlapm

#96 L196:55:196:59 trivial tlapm

▶ <2>2 BY <2>2, <2>4 DEF TypeOK 10/10 tlapm

#84 L188:15:188:17 proved smt

#85 L188:18:188:22 trivial tlapm

#97 L197:44:197:46 proved smt

#98 L197:47:197:51 trivial tlapm

#99 L199:13:199:15 proved smt

#100 L199:16:199:20 trivial tlapm

#101 L199:22:199:26 trivial tlapm

#102 L199:28:199:32 trivial tlapm

#103 L199:34:199:38 trivial tlapm

#104 L199:40:199:44 trivial tlapm

▶ <2>7 <2>7. currentTerm'[t1] = currentTerm[t1] 3/3 tlapm

#156 L243:38:243:40 proved smt

#157 L243:41:243:45 trivial tlapm

#158 L243:47:243:51 trivial tlapm

▶ <2>2 BY <2>2, <2>5 DEF TypeOK 10/10 tlapm

#84 L188:15:188:17 proved smt

#85 L188:18:188:22 trivial tlapm

#97 L197:44:197:46 proved smt

#98 L197:47:197:51 trivial tlapm

#99 L199:13:199:15 proved smt

#100 L199:16:199:20 trivial tlapm

#101 L199:22:199:26 trivial tlapm

#102 L199:28:199:32 trivial tlapm

#103 L199:34:199:38 trivial tlapm

#104 L199:40:199:44 trivial tlapm

▶ <2>8 <2>8. currentTerm[s1] = currentTerm[t1] 11/11 tlapm

#1 L257:11:257:13 proved smt

#2 L257:14:257:18 trivial tlapm

#3 L257:19:257:23 trivial tlapm

#4 L257:24:257:28 trivial tlapm

#5 L257:29:257:33 trivial tlapm

#6 L257:34:257:38 trivial tlapm

#7 L257:39:257:43 trivial tlapm

#40 L200:18:200:20 proved smt

#41 L200:21:200:25 trivial tlapm

#42 L200:27:200:31 trivial tlapm

#43 L200:33:200:37 trivial tlapm

▶ <2>6 BY <2>6, <2>7 6/6 tlapm

#17 L201:16:201:18 proved smt

#18 L201:19:201:23 trivial tlapm

#19 L201:25:201:29 trivial tlapm

#94 L196:46:196:48 proved smt

#95 L196:49:196:53 trivial tlapm

#96 L196:55:196:59 trivial tlapm

▶ <2>4 <2>. QED BY <2>4, <2>5, <2>8 DEF H_OnePrimaryPerTerm 2/2 smt

#90 L192:15:192:17 proved smt

#91 L192:18:192:22 trivial tlapm

▶ <1>7 <1>7. QED BY <1>1,<1>2,<1>3,<1>4,<1>5,<1>6 DEF Next 1/1 smt

#105 L203:94:203:96 proved smt

▶ <1>1 <1>1. TypeOK /\ H_OnePrimaryPerTerm /\ H_PrimaryHasOwnEntries /\ ClientRequestAction => H_PrimaryHasOwnEntries' BY DEF TypeOK,H_OnePrimaryPerTerm,ClientRequestAction,ClientRequest,H_PrimaryHasOwnEntries,InLog 2/2 smt

#109 L210:10:210:12 proved smt

#110 L211:51:211:53 proved smt

▶ <1>2 <1>2. TypeOK /\ H_PrimaryHasOwnEntries /\ GetEntriesAction => H_PrimaryHasOwnEntries' BY DEF TypeOK,GetEntriesAction,GetEntries,H_PrimaryHasOwnEntries,InLog,Empty 1/1 smt

#111 L213:11:213:13 proved smt

▶ <1>3 <1>3. TypeOK /\ H_PrimaryHasOwnEntries /\ RollbackEntriesAction => H_PrimaryHasOwnEntries' BY DEF TypeOK,RollbackEntriesAction,RollbackEntries,H_PrimaryHasOwnEntries,InLog,CanRollback,LastTerm,Empty 1/1 smt

#112 L215:11:215:13 proved smt

▶ <1>4 <1>4. TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ H_PrimaryHasOwnEntries /\ BecomeLeaderAction => H_PrimaryHasOwnEntries' 372/372 smt

#113 L217:11:217:13 proved smt

#114 L218:24:218:26 proved smt

▶ <2>1 <2>1. PICK leader \in Server, Q \in Quorums(Server) : BecomeLeader(leader, Q) 18/18 tlapm

#75 L185:50:185:52 proved smt

#76 L185:53:185:57 trivial tlapm

#77 L185:59:185:63 trivial tlapm

#78 L185:65:185:69 trivial tlapm

#79 L186:54:186:56 proved smt

#80 L186:57:186:61 trivial tlapm

#81 L186:63:186:67 trivial tlapm

#82 L186:69:186:73 trivial tlapm

#83 L186:75:186:79 trivial tlapm

#116 L225:48:225:50 proved smt

#117 L225:51:225:55 trivial tlapm

#124 L229:49:229:51 proved smt

#125 L229:52:229:56 trivial tlapm

#126 L229:58:229:62 trivial tlapm

#127 L229:64:229:68 trivial tlapm

#128 L230:33:230:35 proved smt

#129 L230:36:230:40 trivial tlapm

#130 L230:42:230:46 trivial tlapm

▶ <2>2 <2>2. UNCHANGED <<log, immediatelyCommitted>> 10/10 tlapm

#84 L188:15:188:17 proved smt

#85 L188:18:188:22 trivial tlapm

#97 L197:44:197:46 proved smt

#98 L197:47:197:51 trivial tlapm

#99 L199:13:199:15 proved smt

#100 L199:16:199:20 trivial tlapm

#101 L199:22:199:26 trivial tlapm

#102 L199:28:199:32 trivial tlapm

#103 L199:34:199:38 trivial tlapm

#104 L199:40:199:44 trivial tlapm

▶ <2>1 BY <2>1 DEF BecomeLeader 18/18 tlapm

#75 L185:50:185:52 proved smt

#76 L185:53:185:57 trivial tlapm

#77 L185:59:185:63 trivial tlapm

#78 L185:65:185:69 trivial tlapm

#79 L186:54:186:56 proved smt

#80 L186:57:186:61 trivial tlapm

#81 L186:63:186:67 trivial tlapm

#82 L186:69:186:73 trivial tlapm

#83 L186:75:186:79 trivial tlapm

#116 L225:48:225:50 proved smt

#117 L225:51:225:55 trivial tlapm

#124 L229:49:229:51 proved smt

#125 L229:52:229:56 trivial tlapm

#126 L229:58:229:62 trivial tlapm

#127 L229:64:229:68 trivial tlapm

#128 L230:33:230:35 proved smt

#129 L230:36:230:40 trivial tlapm

#130 L230:42:230:46 trivial tlapm

▶ <2>3 <2>3. \A v \in Q : currentTerm[v] < currentTerm[leader] + 1 11/11 tlapm

#69 L195:19:195:21 proved smt 1.1s (21%)

#70 L195:22:195:26 trivial tlapm

#71 L195:28:195:32 trivial tlapm

#72 L195:34:195:38 trivial tlapm

#73 L195:40:195:44 trivial tlapm

#74 L195:46:195:50 trivial tlapm

#86 L190:15:190:17 proved smt

#87 L190:18:190:22 trivial tlapm

#88 L190:24:190:28 trivial tlapm

#89 L190:30:190:34 trivial tlapm

#115 L224:11:224:13 proved smt

▶ <2>1 BY <2>1 DEF BecomeLeader, CanVoteForOplog 18/18 tlapm

#75 L185:50:185:52 proved smt

#76 L185:53:185:57 trivial tlapm

#77 L185:59:185:63 trivial tlapm

#78 L185:65:185:69 trivial tlapm

#79 L186:54:186:56 proved smt

#80 L186:57:186:61 trivial tlapm

#81 L186:63:186:67 trivial tlapm

#82 L186:69:186:73 trivial tlapm

#83 L186:75:186:79 trivial tlapm

#116 L225:48:225:50 proved smt

#117 L225:51:225:55 trivial tlapm

#124 L229:49:229:51 proved smt

#125 L229:52:229:56 trivial tlapm

#126 L229:58:229:62 trivial tlapm

#127 L229:64:229:68 trivial tlapm

#128 L230:33:230:35 proved smt

#129 L230:36:230:40 trivial tlapm

#130 L230:42:230:46 trivial tlapm

▶ <2>4 <2>4. state' = [s_1 \in Server |-> IF s_1 = leader THEN Primary ELSE IF s_1 \in Q THEN Secondary ELSE state[s_1]] 2/2 smt

#90 L192:15:192:17 proved smt

#91 L192:18:192:22 trivial tlapm

▶ <2>1 BY <2>1 DEF BecomeLeader 18/18 tlapm

#75 L185:50:185:52 proved smt

#76 L185:53:185:57 trivial tlapm

#77 L185:59:185:63 trivial tlapm

#78 L185:65:185:69 trivial tlapm

#79 L186:54:186:56 proved smt

#80 L186:57:186:61 trivial tlapm

#81 L186:63:186:67 trivial tlapm

#82 L186:69:186:73 trivial tlapm

#83 L186:75:186:79 trivial tlapm

#116 L225:48:225:50 proved smt

#117 L225:51:225:55 trivial tlapm

#124 L229:49:229:51 proved smt

#125 L229:52:229:56 trivial tlapm

#126 L229:58:229:62 trivial tlapm

#127 L229:64:229:68 trivial tlapm

#128 L230:33:230:35 proved smt

#129 L230:36:230:40 trivial tlapm

#130 L230:42:230:46 trivial tlapm

▶ <2>5 <2>5. currentTerm' = [s_1 \in Server |-> IF s_1 \in Q THEN currentTerm[leader] + 1 ELSE currentTerm[s_1]] 6/6 tlapm

#92 L194:15:194:17 proved smt

#93 L194:18:194:22 trivial tlapm

#120 L228:55:228:57 proved smt

#121 L228:58:228:62 trivial tlapm

#122 L228:64:228:68 trivial tlapm

#123 L228:70:228:74 trivial tlapm

▶ <2>1 BY <2>1 DEF BecomeLeader 18/18 tlapm

#75 L185:50:185:52 proved smt

#76 L185:53:185:57 trivial tlapm

#77 L185:59:185:63 trivial tlapm

#78 L185:65:185:69 trivial tlapm

#79 L186:54:186:56 proved smt

#80 L186:57:186:61 trivial tlapm

#81 L186:63:186:67 trivial tlapm

#82 L186:69:186:73 trivial tlapm

#83 L186:75:186:79 trivial tlapm

#116 L225:48:225:50 proved smt

#117 L225:51:225:55 trivial tlapm

#124 L229:49:229:51 proved smt

#125 L229:52:229:56 trivial tlapm

#126 L229:58:229:62 trivial tlapm

#127 L229:64:229:68 trivial tlapm

#128 L230:33:230:35 proved smt

#129 L230:36:230:40 trivial tlapm

#130 L230:42:230:46 trivial tlapm

▶ <2>6 <2>6. \A Q1, Q2 \in Quorums(Server) : Q1 \cap Q2 # {} 108/108 tlapm

#17 L201:16:201:18 proved smt

#18 L201:19:201:23 trivial tlapm

#19 L201:25:201:29 trivial tlapm

#94 L196:46:196:48 proved smt

#95 L196:49:196:53 trivial tlapm

#96 L196:55:196:59 trivial tlapm

▶ <3>1 <3>1. IsFiniteSet(Server) BY A0 22/22 tlapm

#25 L163:11:163:13 proved smt

#26 L163:14:163:18 trivial tlapm

#27 L163:20:163:24 trivial tlapm

#46 L173:44:173:46 proved smt

#47 L173:47:173:51 trivial tlapm

#48 L173:53:173:57 trivial tlapm

#118 L240:18:240:20 proved smt

#119 L240:21:240:26 trivial tlapm

#131 L232:13:232:15 proved smt

#132 L232:16:232:20 trivial tlapm

#159 L244:24:244:26 proved smt

#160 L244:27:244:31 trivial tlapm

#161 L244:33:244:37 trivial tlapm

#162 L245:32:245:34 proved smt

#163 L245:35:245:39 trivial tlapm

#164 L245:41:245:45 trivial tlapm

#165 L245:47:245:51 trivial tlapm

#166 L245:53:245:57 trivial tlapm

#170 L247:40:247:42 proved smt

#171 L247:43:247:47 trivial tlapm

#172 L247:49:247:53 trivial tlapm

#173 L247:55:247:59 trivial tlapm

▶ <3>2 <3>2. SUFFICES ASSUME NEW Q1 \in Quorums(Server), NEW Q2 \in Quorums(Server) PROVE Q1 \cap Q2 # {} OBVIOUS 9/9 tlapm

#31 L165:28:165:30 proved smt

#32 L165:31:165:35 trivial tlapm

#33 L165:37:165:41 trivial tlapm

#133 L233:69:233:71 proved smt

#134 L233:72:233:76 trivial tlapm

#135 L233:78:233:82 trivial tlapm

#167 L246:46:246:48 proved smt

#168 L246:49:246:53 trivial tlapm

#169 L246:55:246:59 trivial tlapm

▶ <3>3 <3>3. Q1 \subseteq Server /\ Q2 \subseteq Server BY DEF Quorums 12/12 tlapm

#34 L167:7:167:9 proved smt

#35 L167:10:167:14 trivial tlapm

#36 L167:16:167:20 trivial tlapm

#37 L167:22:167:26 trivial tlapm

#38 L167:28:167:32 trivial tlapm

#39 L167:34:167:38 trivial tlapm

#45 L172:13:172:15 proved smt

#136 L234:28:234:30 proved smt

#137 L234:31:234:47 trivial tlapm

#174 L248:33:248:35 proved smt

#175 L248:36:248:40 trivial tlapm

#176 L248:42:248:46 trivial tlapm

▶ <3>4 <3>4. IsFiniteSet(Q1) /\ IsFiniteSet(Q2) BY <3>1, <3>3, FS_Subset 11/11 tlapm

#44 L169:60:169:62 proved smt

#106 L252:16:252:18 proved smt

#107 L252:19:252:23 trivial tlapm

#108 L252:25:252:29 trivial tlapm

#138 L235:41:235:43 proved smt

#139 L235:44:235:48 trivial tlapm

#177 L250:13:250:15 proved smt

#178 L250:16:250:20 trivial tlapm

#179 L250:22:250:26 trivial tlapm

#180 L250:28:250:32 trivial tlapm

#181 L254:90:254:92 proved smt

▶ <3>5 <3>5. Cardinality(Q1) * 2 > Cardinality(Server) /\ Cardinality(Q2) * 2 > Cardinality(Server) BY DEF Quorums 7/7 tlapm

#140 L236:54:236:56 proved smt

#141 L236:57:236:61 trivial tlapm

#142 L236:63:236:67 trivial tlapm

#153 L251:17:251:19 proved smt

#154 L251:20:251:24 trivial tlapm

#155 L251:26:251:30 trivial tlapm

#182 L256:90:256:92 proved smt

▶ <3>6 <3>6. Cardinality(Server) \in Nat BY <3>1, FS_CardinalityType 11/11 tlapm

#8 L144:12:144:14 trivial tlapm

#9 L144:15:144:17 trivial tlapm

#10 L144:18:144:20 trivial tlapm

#11 L144:21:144:23 trivial tlapm

#12 L144:24:144:26 trivial tlapm

#13 L144:27:144:29 trivial tlapm

#14 L144:30:144:32 trivial tlapm

#15 L144:33:144:55 trivial tlapm

#143 L237:55:237:57 proved smt

#144 L237:58:237:62 trivial tlapm

#145 L237:64:237:68 trivial tlapm

▶ <3>7 <3>7. Cardinality(Q1) \in Nat /\ Cardinality(Q2) \in Nat BY <3>4, FS_CardinalityType 4/4 smt

#16 L146:115:146:117 proved smt

#146 L238:68:238:70 proved smt

#147 L238:71:238:75 trivial tlapm

#148 L238:77:238:81 trivial tlapm

▶ <3>8 <3>8. Cardinality(Q1) + Cardinality(Q2) > Cardinality(Server) BY <3>5, <3>6, <3>7 4/4 tlapm

#149 L239:20:239:22 proved smt

#150 L239:23:239:27 trivial tlapm

#151 L239:29:239:33 trivial tlapm

#152 L239:35:239:40 trivial tlapm

▶ <3>1 <3>. QED BY <3>1, <3>3, <3>8, FS_MajoritiesIntersect 22/22 tlapm

#25 L163:11:163:13 proved smt

#26 L163:14:163:18 trivial tlapm

#27 L163:20:163:24 trivial tlapm

#46 L173:44:173:46 proved smt

#47 L173:47:173:51 trivial tlapm

#48 L173:53:173:57 trivial tlapm

#118 L240:18:240:20 proved smt

#119 L240:21:240:26 trivial tlapm

#131 L232:13:232:15 proved smt

#132 L232:16:232:20 trivial tlapm

#159 L244:24:244:26 proved smt

#160 L244:27:244:31 trivial tlapm

#161 L244:33:244:37 trivial tlapm

#162 L245:32:245:34 proved smt

#163 L245:35:245:39 trivial tlapm

#164 L245:41:245:45 trivial tlapm

#165 L245:47:245:51 trivial tlapm

#166 L245:53:245:57 trivial tlapm

#170 L247:40:247:42 proved smt

#171 L247:43:247:47 trivial tlapm

#172 L247:49:247:53 trivial tlapm

#173 L247:55:247:59 trivial tlapm

▶ <2>7 <2>7. \A s \in Server : \A k \in DOMAIN log[s] : log[s][k] # currentTerm[leader] + 1 68/68 tlapm

#156 L243:38:243:40 proved smt

#157 L243:41:243:45 trivial tlapm

#158 L243:47:243:51 trivial tlapm

▶ <3>1 <3>1. PICK Qe \in Quorums(Server) : \A n \in Qe : currentTerm[n] >= log[s][k] 22/22 tlapm

#25 L163:11:163:13 proved smt

#26 L163:14:163:18 trivial tlapm

#27 L163:20:163:24 trivial tlapm

#46 L173:44:173:46 proved smt

#47 L173:47:173:51 trivial tlapm

#48 L173:53:173:57 trivial tlapm

#118 L240:18:240:20 proved smt

#119 L240:21:240:26 trivial tlapm

#131 L232:13:232:15 proved smt

#132 L232:16:232:20 trivial tlapm

#159 L244:24:244:26 proved smt

#160 L244:27:244:31 trivial tlapm

#161 L244:33:244:37 trivial tlapm

#162 L245:32:245:34 proved smt

#163 L245:35:245:39 trivial tlapm

#164 L245:41:245:45 trivial tlapm

#165 L245:47:245:51 trivial tlapm

#166 L245:53:245:57 trivial tlapm

#170 L247:40:247:42 proved smt

#171 L247:43:247:47 trivial tlapm

#172 L247:49:247:53 trivial tlapm

#173 L247:55:247:59 trivial tlapm

▶ <3>2 <3>2. \A n \in Qe : currentTerm[n] >= currentTerm[leader] + 1 9/9 tlapm

#31 L165:28:165:30 proved smt

#32 L165:31:165:35 trivial tlapm

#33 L165:37:165:41 trivial tlapm

#133 L233:69:233:71 proved smt

#134 L233:72:233:76 trivial tlapm

#135 L233:78:233:82 trivial tlapm

#167 L246:46:246:48 proved smt

#168 L246:49:246:53 trivial tlapm

#169 L246:55:246:59 trivial tlapm

▶ <3>1 BY <3>1 22/22 tlapm

#25 L163:11:163:13 proved smt

#26 L163:14:163:18 trivial tlapm

#27 L163:20:163:24 trivial tlapm

#46 L173:44:173:46 proved smt

#47 L173:47:173:51 trivial tlapm

#48 L173:53:173:57 trivial tlapm

#118 L240:18:240:20 proved smt

#119 L240:21:240:26 trivial tlapm

#131 L232:13:232:15 proved smt

#132 L232:16:232:20 trivial tlapm

#159 L244:24:244:26 proved smt

#160 L244:27:244:31 trivial tlapm

#161 L244:33:244:37 trivial tlapm

#162 L245:32:245:34 proved smt

#163 L245:35:245:39 trivial tlapm

#164 L245:41:245:45 trivial tlapm

#165 L245:47:245:51 trivial tlapm

#166 L245:53:245:57 trivial tlapm

#170 L247:40:247:42 proved smt

#171 L247:43:247:47 trivial tlapm

#172 L247:49:247:53 trivial tlapm

#173 L247:55:247:59 trivial tlapm

▶ <3>3 <3>3. Q \cap Qe # {} 12/12 tlapm

#34 L167:7:167:9 proved smt

#35 L167:10:167:14 trivial tlapm

#36 L167:16:167:20 trivial tlapm

#37 L167:22:167:26 trivial tlapm

#38 L167:28:167:32 trivial tlapm

#39 L167:34:167:38 trivial tlapm

#45 L172:13:172:15 proved smt

#136 L234:28:234:30 proved smt

#137 L234:31:234:47 trivial tlapm

#174 L248:33:248:35 proved smt

#175 L248:36:248:40 trivial tlapm

#176 L248:42:248:46 trivial tlapm

▶ <2>6 BY <2>6 64/64 tlapm

#17 L201:16:201:18 proved smt

#18 L201:19:201:23 trivial tlapm

#19 L201:25:201:29 trivial tlapm

#94 L196:46:196:48 proved smt

#95 L196:49:196:53 trivial tlapm

#96 L196:55:196:59 trivial tlapm

▶ <3>4 <3>4. PICK w \in Q \cap Qe : TRUE BY <3>3 11/11 tlapm

#44 L169:60:169:62 proved smt

#106 L252:16:252:18 proved smt

#107 L252:19:252:23 trivial tlapm

#108 L252:25:252:29 trivial tlapm

#138 L235:41:235:43 proved smt

#139 L235:44:235:48 trivial tlapm

#177 L250:13:250:15 proved smt

#178 L250:16:250:20 trivial tlapm

#179 L250:22:250:26 trivial tlapm

#180 L250:28:250:32 trivial tlapm

#181 L254:90:254:92 proved smt

▶ <3>5 <3>5. currentTerm[w] < currentTerm[leader] + 1 7/7 tlapm

#140 L236:54:236:56 proved smt

#141 L236:57:236:61 trivial tlapm

#142 L236:63:236:67 trivial tlapm

#153 L251:17:251:19 proved smt

#154 L251:20:251:24 trivial tlapm

#155 L251:26:251:30 trivial tlapm

#182 L256:90:256:92 proved smt

▶ <3>4 BY <3>4, <2>3 11/11 tlapm

#44 L169:60:169:62 proved smt

#106 L252:16:252:18 proved smt

#107 L252:19:252:23 trivial tlapm

#108 L252:25:252:29 trivial tlapm

#138 L235:41:235:43 proved smt

#139 L235:44:235:48 trivial tlapm

#177 L250:13:250:15 proved smt

#178 L250:16:250:20 trivial tlapm

#179 L250:22:250:26 trivial tlapm

#180 L250:28:250:32 trivial tlapm

#181 L254:90:254:92 proved smt

▶ <3>6 <3>6. currentTerm[w] >= currentTerm[leader] + 1 11/11 tlapm

#8 L144:12:144:14 trivial tlapm

#9 L144:15:144:17 trivial tlapm

#10 L144:18:144:20 trivial tlapm

#11 L144:21:144:23 trivial tlapm

#12 L144:24:144:26 trivial tlapm

#13 L144:27:144:29 trivial tlapm

#14 L144:30:144:32 trivial tlapm

#15 L144:33:144:55 trivial tlapm

#143 L237:55:237:57 proved smt

#144 L237:58:237:62 trivial tlapm

#145 L237:64:237:68 trivial tlapm

▶ <3>4 BY <3>4, <3>2 11/11 tlapm

#44 L169:60:169:62 proved smt

#106 L252:16:252:18 proved smt

#107 L252:19:252:23 trivial tlapm

#108 L252:25:252:29 trivial tlapm

#138 L235:41:235:43 proved smt

#139 L235:44:235:48 trivial tlapm

#177 L250:13:250:15 proved smt

#178 L250:16:250:20 trivial tlapm

#179 L250:22:250:26 trivial tlapm

#180 L250:28:250:32 trivial tlapm

#181 L254:90:254:92 proved smt

▶ <3>5 <3>. QED BY <3>5, <3>6 DEF TypeOK, Terms 7/7 tlapm

#140 L236:54:236:56 proved smt

#141 L236:57:236:61 trivial tlapm

#142 L236:63:236:67 trivial tlapm

#153 L251:17:251:19 proved smt

#154 L251:20:251:24 trivial tlapm

#155 L251:26:251:30 trivial tlapm

#182 L256:90:256:92 proved smt

▶ <2>8 <2>8. \A j \in Server : \A k \in DOMAIN log'[j] : log'[j][k] # currentTerm'[leader] 11/11 tlapm

#1 L257:11:257:13 proved smt

#2 L257:14:257:18 trivial tlapm

#3 L257:19:257:23 trivial tlapm

#4 L257:24:257:28 trivial tlapm

#5 L257:29:257:33 trivial tlapm

#6 L257:34:257:38 trivial tlapm

#7 L257:39:257:43 trivial tlapm

#40 L200:18:200:20 proved smt

#41 L200:21:200:25 trivial tlapm

#42 L200:27:200:31 trivial tlapm

#43 L200:33:200:37 trivial tlapm

THEOREM L_2 (H_PrimaryHasOwnEntries)

Proof Tree