Proof Status: THEOREM L

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

#26 L75:10:75:12 proved smt 0.1s (1%)

#27 L76:24:76:26 proved smt 0.3s (7%)

#31 L83:11:83:13 proved smt 0.2s (4%)

#32 L83:14:83:18 trivial tlapm

#73 L108:13:108:15 proved smt 0.5s (10%)

#74 L108:16:108:20 trivial tlapm

#75 L108:22:108:26 trivial tlapm

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

#28 L77:76:77:78 proved smt 0.3s (6%)

▶ <2>1 BY <2>1 DEF BecomeLeader, CanVoteForOplog 7/7 smt

#26 L75:10:75:12 proved smt 0.1s (1%)

#27 L76:24:76:26 proved smt 0.3s (7%)

#31 L83:11:83:13 proved smt 0.2s (4%)

#32 L83:14:83:18 trivial tlapm

#73 L108:13:108:15 proved smt 0.5s (10%)

#74 L108:16:108:20 trivial tlapm

#75 L108:22:108:26 trivial tlapm

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

#29 L79:11:79:13 proved smt 0.3s (5%)

▶ <2>1 BY <2>1 DEF BecomeLeader 7/7 smt

#26 L75:10:75:12 proved smt 0.1s (1%)

#27 L76:24:76:26 proved smt 0.3s (7%)

#31 L83:11:83:13 proved smt 0.2s (4%)

#32 L83:14:83:18 trivial tlapm

#73 L108:13:108:15 proved smt 0.5s (10%)

#74 L108:16:108:20 trivial tlapm

#75 L108:22:108:26 trivial tlapm

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

#30 L81:11:81:13 proved smt 0.2s (4%)

▶ <2>1 BY <2>1 DEF BecomeLeader 7/7 smt

#26 L75:10:75:12 proved smt 0.1s (1%)

#27 L76:24:76:26 proved smt 0.3s (7%)

#31 L83:11:83:13 proved smt 0.2s (4%)

#32 L83:14:83:18 trivial tlapm

#73 L108:13:108:15 proved smt 0.5s (10%)

#74 L108:16:108:20 trivial tlapm

#75 L108:22:108:26 trivial tlapm

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

#98 L118:69:118:71 proved smt 0.8s (16%)

#99 L118:72:118:76 trivial tlapm

#100 L118:78:118:82 trivial tlapm

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

#1 L139:11:139:13 proved smt 0.9s (18%)

#2 L139:14:139:18 trivial tlapm

#3 L139:19:139:23 trivial tlapm

#4 L139:24:139:28 trivial tlapm

#5 L139:29:139:33 trivial tlapm

#6 L139:34:139:38 trivial tlapm

#7 L139:39:139:43 trivial tlapm

#19 L134:16:134:18 proved smt 0.2s (3%)

#20 L134:19:134:23 trivial tlapm

#21 L134:25:134:29 trivial tlapm

#22 L134:31:134:35 trivial tlapm

#23 L134:37:134:42 trivial tlapm

#24 L134:44:134:49 trivial tlapm

#25 L134:51:134:56 trivial tlapm

#40 L94:11:94:13 proved smt 0.4s (7%)

#41 L94:14:94:18 trivial tlapm

#54 L99:55:99:57 proved zenon 0.1s (1%)

#55 L99:58:99:62 trivial tlapm

#56 L99:64:99:68 trivial tlapm

#57 L99:70:99:74 trivial tlapm

#60 L102:69:102:71 proved smt 0.3s (7%)

#61 L102:72:102:76 trivial tlapm

#62 L102:78:102:82 trivial tlapm

#65 L104:41:104:43 proved smt 0.2s (4%)

#66 L104:44:104:48 trivial tlapm

▶ <3>2 <3>2. IsFiniteSet(Server) BY A0 6/6 smt

#58 L101:13:101:15 proved smt 0.4s (8%)

#59 L101:16:101:20 trivial tlapm

#70 L106:56:106:58 proved smt 0.1s (2%)

#71 L106:59:106:63 trivial tlapm

#72 L106:65:106:69 trivial tlapm

#138 L136:84:136:86 proved smt 0.1s (3%)

▶ <3>3 <3>3. IsFiniteSet(Q1) /\ IsFiniteSet(Q2) BY <3>1, <3>2, FS_Subset 8/8 smt

#33 L88:11:88:13 proved smt 0.1s (2%)

#63 L103:28:103:30 proved smt 0.3s (5%)

#64 L103:31:103:47 trivial tlapm

#92 L115:55:115:57 proved smt 0.1s (2%)

#93 L115:58:115:62 trivial tlapm

#94 L115:64:115:68 trivial tlapm

#95 L115:70:115:74 trivial tlapm

#139 L138:84:138:86 proved smt 0.1s (3%)

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

#67 L105:54:105:56 proved smt 0.2s (3%)

#68 L105:57:105:61 trivial tlapm

#69 L105:63:105:67 trivial tlapm

#82 L112:48:112:50 proved smt 0.3s (6%)

#83 L112:51:112:55 trivial tlapm

#84 L112:57:112:62 trivial tlapm

#85 L113:56:113:58 proved smt 0.2s (5%)

#86 L113:59:113:63 trivial tlapm

#87 L113:65:113:69 trivial tlapm

#88 L113:71:113:76 trivial tlapm

▶ <3>5 <3>5. Cardinality(Server) \in Nat BY <3>2, FS_CardinalityType 3/3 tlapm

#34 L90:11:90:13 proved smt 0.1s (1%)

#35 L90:14:90:18 trivial tlapm

#36 L90:20:90:24 trivial tlapm

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

#76 L109:20:109:22 proved smt 0.4s (8%)

#77 L109:23:109:27 trivial tlapm

#78 L109:29:109:34 trivial tlapm

#79 L109:36:109:41 trivial tlapm

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

#37 L92:11:92:13 proved smt 0.4s (8%)

#38 L92:14:92:18 trivial tlapm

#39 L92:20:92:24 trivial tlapm

#122 L128:48:128:50 proved smt 0.5s (9%)

#123 L128:51:128:55 trivial tlapm

#124 L128:57:128:62 trivial tlapm

▶ <3>1 <3>. QED BY <3>1, <3>2, <3>7, FS_MajoritiesIntersect 25/25 tlapm

#1 L139:11:139:13 proved smt 0.9s (18%)

#2 L139:14:139:18 trivial tlapm

#3 L139:19:139:23 trivial tlapm

#4 L139:24:139:28 trivial tlapm

#5 L139:29:139:33 trivial tlapm

#6 L139:34:139:38 trivial tlapm

#7 L139:39:139:43 trivial tlapm

#19 L134:16:134:18 proved smt 0.2s (3%)

#20 L134:19:134:23 trivial tlapm

#21 L134:25:134:29 trivial tlapm

#22 L134:31:134:35 trivial tlapm

#23 L134:37:134:42 trivial tlapm

#24 L134:44:134:49 trivial tlapm

#25 L134:51:134:56 trivial tlapm

#40 L94:11:94:13 proved smt 0.4s (7%)

#41 L94:14:94:18 trivial tlapm

#54 L99:55:99:57 proved zenon 0.1s (1%)

#55 L99:58:99:62 trivial tlapm

#56 L99:64:99:68 trivial tlapm

#57 L99:70:99:74 trivial tlapm

#60 L102:69:102:71 proved smt 0.3s (7%)

#61 L102:72:102:76 trivial tlapm

#62 L102:78:102:82 trivial tlapm

#65 L104:41:104:43 proved smt 0.2s (4%)

#66 L104:44:104:48 trivial tlapm

▶ <2>6 <2>6. CASE s1 = leader /\ t1 = leader 7/7 tlapm

#44 L96:48:96:50 proved smt 0.3s (5%)

#45 L96:51:96:55 trivial tlapm

#46 L96:57:96:62 trivial tlapm

#47 L97:56:97:58 proved smt 0.2s (4%)

#48 L97:59:97:63 trivial tlapm

#49 L97:65:97:69 trivial tlapm

#50 L97:71:97:76 trivial tlapm

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

#44 L96:48:96:50 proved smt 0.3s (5%)

#45 L96:51:96:55 trivial tlapm

#46 L96:57:96:62 trivial tlapm

#47 L97:56:97:58 proved smt 0.2s (4%)

#48 L97:59:97:63 trivial tlapm

#49 L97:65:97:69 trivial tlapm

#50 L97:71:97:76 trivial tlapm

▶ <2>7 <2>7. CASE s1 = leader /\ t1 # leader 30/30 tlapm

#42 L110:18:110:20 proved smt 0.3s (6%)

#43 L110:21:110:26 trivial tlapm

#51 L98:48:98:50 proved smt 0.1s (3%)

#52 L98:51:98:55 trivial tlapm

#53 L98:57:98:61 trivial tlapm

▶ <3>1 <3>1. state'[t1] = Primary /\ t1 # leader 25/25 tlapm

#1 L139:11:139:13 proved smt 0.9s (18%)

#2 L139:14:139:18 trivial tlapm

#3 L139:19:139:23 trivial tlapm

#4 L139:24:139:28 trivial tlapm

#5 L139:29:139:33 trivial tlapm

#6 L139:34:139:38 trivial tlapm

#7 L139:39:139:43 trivial tlapm

#19 L134:16:134:18 proved smt 0.2s (3%)

#20 L134:19:134:23 trivial tlapm

#21 L134:25:134:29 trivial tlapm

#22 L134:31:134:35 trivial tlapm

#23 L134:37:134:42 trivial tlapm

#24 L134:44:134:49 trivial tlapm

#25 L134:51:134:56 trivial tlapm

#40 L94:11:94:13 proved smt 0.4s (7%)

#41 L94:14:94:18 trivial tlapm

#54 L99:55:99:57 proved zenon 0.1s (1%)

#55 L99:58:99:62 trivial tlapm

#56 L99:64:99:68 trivial tlapm

#57 L99:70:99:74 trivial tlapm

#60 L102:69:102:71 proved smt 0.3s (7%)

#61 L102:72:102:76 trivial tlapm

#62 L102:78:102:82 trivial tlapm

#65 L104:41:104:43 proved smt 0.2s (4%)

#66 L104:44:104:48 trivial tlapm

▶ <2>7 BY <2>7 88/88 tlapm

#42 L110:18:110:20 proved smt 0.3s (6%)

#43 L110:21:110:26 trivial tlapm

#51 L98:48:98:50 proved smt 0.1s (3%)

#52 L98:51:98:55 trivial tlapm

#53 L98:57:98:61 trivial tlapm

▶ <3>2 <3>2. t1 \notin Q 6/6 smt

#58 L101:13:101:15 proved smt 0.4s (8%)

#59 L101:16:101:20 trivial tlapm

#70 L106:56:106:58 proved smt 0.1s (2%)

#71 L106:59:106:63 trivial tlapm

#72 L106:65:106:69 trivial tlapm

#138 L136:84:136:86 proved smt 0.1s (3%)

▶ <3>1 BY <3>1, <2>3 25/25 tlapm

#1 L139:11:139:13 proved smt 0.9s (18%)

#2 L139:14:139:18 trivial tlapm

#3 L139:19:139:23 trivial tlapm

#4 L139:24:139:28 trivial tlapm

#5 L139:29:139:33 trivial tlapm

#6 L139:34:139:38 trivial tlapm

#7 L139:39:139:43 trivial tlapm

#19 L134:16:134:18 proved smt 0.2s (3%)

#20 L134:19:134:23 trivial tlapm

#21 L134:25:134:29 trivial tlapm

#22 L134:31:134:35 trivial tlapm

#23 L134:37:134:42 trivial tlapm

#24 L134:44:134:49 trivial tlapm

#25 L134:51:134:56 trivial tlapm

#40 L94:11:94:13 proved smt 0.4s (7%)

#41 L94:14:94:18 trivial tlapm

#54 L99:55:99:57 proved zenon 0.1s (1%)

#55 L99:58:99:62 trivial tlapm

#56 L99:64:99:68 trivial tlapm

#57 L99:70:99:74 trivial tlapm

#60 L102:69:102:71 proved smt 0.3s (7%)

#61 L102:72:102:76 trivial tlapm

#62 L102:78:102:82 trivial tlapm

#65 L104:41:104:43 proved smt 0.2s (4%)

#66 L104:44:104:48 trivial tlapm

▶ <3>3 <3>3. state[t1] = Primary 8/8 smt

#33 L88:11:88:13 proved smt 0.1s (2%)

#63 L103:28:103:30 proved smt 0.3s (5%)

#64 L103:31:103:47 trivial tlapm

#92 L115:55:115:57 proved smt 0.1s (2%)

#93 L115:58:115:62 trivial tlapm

#94 L115:64:115:68 trivial tlapm

#95 L115:70:115:74 trivial tlapm

#139 L138:84:138:86 proved smt 0.1s (3%)

▶ <3>1 BY <3>1, <3>2, <2>3 25/25 tlapm

#1 L139:11:139:13 proved smt 0.9s (18%)

#2 L139:14:139:18 trivial tlapm

#3 L139:19:139:23 trivial tlapm

#4 L139:24:139:28 trivial tlapm

#5 L139:29:139:33 trivial tlapm

#6 L139:34:139:38 trivial tlapm

#7 L139:39:139:43 trivial tlapm

#19 L134:16:134:18 proved smt 0.2s (3%)

#20 L134:19:134:23 trivial tlapm

#21 L134:25:134:29 trivial tlapm

#22 L134:31:134:35 trivial tlapm

#23 L134:37:134:42 trivial tlapm

#24 L134:44:134:49 trivial tlapm

#25 L134:51:134:56 trivial tlapm

#40 L94:11:94:13 proved smt 0.4s (7%)

#41 L94:14:94:18 trivial tlapm

#54 L99:55:99:57 proved zenon 0.1s (1%)

#55 L99:58:99:62 trivial tlapm

#56 L99:64:99:68 trivial tlapm

#57 L99:70:99:74 trivial tlapm

#60 L102:69:102:71 proved smt 0.3s (7%)

#61 L102:72:102:76 trivial tlapm

#62 L102:78:102:82 trivial tlapm

#65 L104:41:104:43 proved smt 0.2s (4%)

#66 L104:44:104:48 trivial tlapm

▶ <3>4 <3>4. currentTerm'[t1] = currentTerm[t1] 10/10 tlapm

#67 L105:54:105:56 proved smt 0.2s (3%)

#68 L105:57:105:61 trivial tlapm

#69 L105:63:105:67 trivial tlapm

#82 L112:48:112:50 proved smt 0.3s (6%)

#83 L112:51:112:55 trivial tlapm

#84 L112:57:112:62 trivial tlapm

#85 L113:56:113:58 proved smt 0.2s (5%)

#86 L113:59:113:63 trivial tlapm

#87 L113:65:113:69 trivial tlapm

#88 L113:71:113:76 trivial tlapm

▶ <3>2 BY <3>2, <2>4 6/6 smt

#58 L101:13:101:15 proved smt 0.4s (8%)

#59 L101:16:101:20 trivial tlapm

#70 L106:56:106:58 proved smt 0.1s (2%)

#71 L106:59:106:63 trivial tlapm

#72 L106:65:106:69 trivial tlapm

#138 L136:84:136:86 proved smt 0.1s (3%)

▶ <3>5 <3>5. leader \in Q 3/3 tlapm

#34 L90:11:90:13 proved smt 0.1s (1%)

#35 L90:14:90:18 trivial tlapm

#36 L90:20:90:24 trivial tlapm

▶ <2>1 BY <2>1 DEF BecomeLeader 11/11 smt

#26 L75:10:75:12 proved smt 0.1s (1%)

#27 L76:24:76:26 proved smt 0.3s (7%)

#31 L83:11:83:13 proved smt 0.2s (4%)

#32 L83:14:83:18 trivial tlapm

#73 L108:13:108:15 proved smt 0.5s (10%)

#74 L108:16:108:20 trivial tlapm

#75 L108:22:108:26 trivial tlapm

▶ <3>6 <3>6. currentTerm'[s1] = currentTerm[leader] + 1 4/4 tlapm

#76 L109:20:109:22 proved smt 0.4s (8%)

#77 L109:23:109:27 trivial tlapm

#78 L109:29:109:34 trivial tlapm

#79 L109:36:109:41 trivial tlapm

▶ <2>7 BY <2>7, <3>5, <2>4 39/39 tlapm

#42 L110:18:110:20 proved smt 0.3s (6%)

#43 L110:21:110:26 trivial tlapm

#51 L98:48:98:50 proved smt 0.1s (3%)

#52 L98:51:98:55 trivial tlapm

#53 L98:57:98:61 trivial tlapm

▶ <3>7 <3>7. currentTerm[t1] = currentTerm[leader] + 1 6/6 tlapm

#37 L92:11:92:13 proved smt 0.4s (8%)

#38 L92:14:92:18 trivial tlapm

#39 L92:20:92:24 trivial tlapm

#122 L128:48:128:50 proved smt 0.5s (9%)

#123 L128:51:128:55 trivial tlapm

#124 L128:57:128:62 trivial tlapm

▶ <3>4 BY <3>4, <3>6 10/10 tlapm

#67 L105:54:105:56 proved smt 0.2s (3%)

#68 L105:57:105:61 trivial tlapm

#69 L105:63:105:67 trivial tlapm

#82 L112:48:112:50 proved smt 0.3s (6%)

#83 L112:51:112:55 trivial tlapm

#84 L112:57:112:62 trivial tlapm

#85 L113:56:113:58 proved smt 0.2s (5%)

#86 L113:59:113:63 trivial tlapm

#87 L113:65:113:69 trivial tlapm

#88 L113:71:113:76 trivial tlapm

▶ <3>8 <3>8. PICK Qt \in Quorums(Server) : \A n \in Qt : currentTerm[n] >= currentTerm[t1] 3/3 tlapm

#89 L114:48:114:50 proved smt 0.2s (3%)

#90 L114:51:114:55 trivial tlapm

#91 L114:57:114:61 trivial tlapm

▶ <3>3 BY <3>3 DEF H_QuorumsSafeAtTerms 8/8 smt

#33 L88:11:88:13 proved smt 0.1s (2%)

#63 L103:28:103:30 proved smt 0.3s (5%)

#64 L103:31:103:47 trivial tlapm

#92 L115:55:115:57 proved smt 0.1s (2%)

#93 L115:58:115:62 trivial tlapm

#94 L115:64:115:68 trivial tlapm

#95 L115:70:115:74 trivial tlapm

#139 L138:84:138:86 proved smt 0.1s (3%)

▶ <3>9 <3>9. Q \cap Qt # {} 7/7 tlapm

#96 L117:13:117:15 proved smt 0.9s (18%)

#97 L117:16:117:20 trivial tlapm

#103 L120:41:120:43 proved smt

#104 L120:44:120:48 trivial tlapm

#105 L121:54:121:56 proved smt

#106 L121:57:121:61 trivial tlapm

#107 L121:63:121:67 trivial tlapm

▶ <2>5 BY <2>5 73/73 tlapm

#98 L118:69:118:71 proved smt 0.8s (16%)

#99 L118:72:118:76 trivial tlapm

#100 L118:78:118:82 trivial tlapm

▶ <3>10 <3>10. PICK w \in Q \cap Qt : TRUE 7/7 tlapm

#80 L126:18:126:20 proved smt

#81 L126:21:126:26 trivial tlapm

#101 L119:28:119:30 proved smt

#102 L119:31:119:47 trivial tlapm

#111 L124:13:124:15 proved smt

#112 L124:16:124:20 trivial tlapm

#113 L124:22:124:26 trivial tlapm

▶ <3>9 BY <3>9 7/7 tlapm

#96 L117:13:117:15 proved smt 0.9s (18%)

#97 L117:16:117:20 trivial tlapm

#103 L120:41:120:43 proved smt

#104 L120:44:120:48 trivial tlapm

#105 L121:54:121:56 proved smt

#106 L121:57:121:61 trivial tlapm

#107 L121:63:121:67 trivial tlapm

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

#108 L122:56:122:58 proved smt

#109 L122:59:122:63 trivial tlapm

#110 L122:65:122:69 trivial tlapm

#128 L130:48:130:50 proved smt

#129 L130:51:130:55 trivial tlapm

#130 L130:57:130:61 trivial tlapm

▶ <3>10 BY <3>10, <2>2 7/7 tlapm

#80 L126:18:126:20 proved smt

#81 L126:21:126:26 trivial tlapm

#101 L119:28:119:30 proved smt

#102 L119:31:119:47 trivial tlapm

#111 L124:13:124:15 proved smt

#112 L124:16:124:20 trivial tlapm

#113 L124:22:124:26 trivial tlapm

▶ <3>12 <3>12. currentTerm[w] >= currentTerm[t1] 4/4 tlapm

#114 L125:20:125:22 proved smt

#115 L125:23:125:27 trivial tlapm

#116 L125:29:125:34 trivial tlapm

#117 L125:36:125:41 trivial tlapm

▶ <3>10 BY <3>10, <3>8 7/7 tlapm

#80 L126:18:126:20 proved smt

#81 L126:21:126:26 trivial tlapm

#101 L119:28:119:30 proved smt

#102 L119:31:119:47 trivial tlapm

#111 L124:13:124:15 proved smt

#112 L124:16:124:20 trivial tlapm

#113 L124:22:124:26 trivial tlapm

▶ <3>13 <3>13. currentTerm[w] >= currentTerm[leader] + 1

▶ <3>7 BY <3>7, <3>12 6/6 tlapm

#37 L92:11:92:13 proved smt 0.4s (8%)

#38 L92:14:92:18 trivial tlapm

#39 L92:20:92:24 trivial tlapm

#122 L128:48:128:50 proved smt 0.5s (9%)

#123 L128:51:128:55 trivial tlapm

#124 L128:57:128:62 trivial tlapm

▶ <3>14 <3>14. FALSE 10/10 tlapm

#125 L129:48:129:50 proved smt 0.4s (8%)

#126 L129:51:129:55 trivial tlapm

#127 L129:57:129:62 trivial tlapm

#131 L131:48:131:50 proved smt

#132 L131:51:131:55 trivial tlapm

#133 L131:57:131:61 trivial tlapm

#134 L132:47:132:49 proved zenon 0.1s (1%)

#135 L132:50:132:54 trivial tlapm

#136 L132:56:132:60 trivial tlapm

#137 L132:62:132:66 trivial tlapm

▶ <3>11 BY <3>11, <3>13 DEF TypeOK, Terms 6/6 tlapm

#108 L122:56:122:58 proved smt

#109 L122:59:122:63 trivial tlapm

#110 L122:65:122:69 trivial tlapm

#128 L130:48:130:50 proved smt

#129 L130:51:130:55 trivial tlapm

#130 L130:57:130:61 trivial tlapm

▶ <3>14 <3>. QED BY <3>14 10/10 tlapm

#125 L129:48:129:50 proved smt 0.4s (8%)

#126 L129:51:129:55 trivial tlapm

#127 L129:57:129:62 trivial tlapm

#131 L131:48:131:50 proved smt

#132 L131:51:131:55 trivial tlapm

#133 L131:57:131:61 trivial tlapm

#134 L132:47:132:49 proved zenon 0.1s (1%)

#135 L132:50:132:54 trivial tlapm

#136 L132:56:132:60 trivial tlapm

#137 L132:62:132:66 trivial tlapm

▶ <2>8 <2>8. CASE s1 # leader /\ t1 = leader 29/29 tlapm

#118 L133:17:133:19 proved smt 0.6s (11%)

#119 L133:20:133:24 trivial tlapm

#120 L133:26:133:30 trivial tlapm

#121 L133:32:133:36 trivial tlapm

▶ <3>1 <3>1. s1 \notin Q 25/25 tlapm

#1 L139:11:139:13 proved smt 0.9s (18%)

#2 L139:14:139:18 trivial tlapm

#3 L139:19:139:23 trivial tlapm

#4 L139:24:139:28 trivial tlapm

#5 L139:29:139:33 trivial tlapm

#6 L139:34:139:38 trivial tlapm

#7 L139:39:139:43 trivial tlapm

#19 L134:16:134:18 proved smt 0.2s (3%)

#20 L134:19:134:23 trivial tlapm

#21 L134:25:134:29 trivial tlapm

#22 L134:31:134:35 trivial tlapm

#23 L134:37:134:42 trivial tlapm

#24 L134:44:134:49 trivial tlapm

#25 L134:51:134:56 trivial tlapm

#40 L94:11:94:13 proved smt 0.4s (7%)

#41 L94:14:94:18 trivial tlapm

#54 L99:55:99:57 proved zenon 0.1s (1%)

#55 L99:58:99:62 trivial tlapm

#56 L99:64:99:68 trivial tlapm

#57 L99:70:99:74 trivial tlapm

#60 L102:69:102:71 proved smt 0.3s (7%)

#61 L102:72:102:76 trivial tlapm

#62 L102:78:102:82 trivial tlapm

#65 L104:41:104:43 proved smt 0.2s (4%)

#66 L104:44:104:48 trivial tlapm

▶ <2>8 BY <2>8, <2>3 10/10 tlapm

#118 L133:17:133:19 proved smt 0.6s (11%)

#119 L133:20:133:24 trivial tlapm

#120 L133:26:133:30 trivial tlapm

#121 L133:32:133:36 trivial tlapm

▶ <3>2 <3>2. state[s1] = Primary 6/6 smt

#58 L101:13:101:15 proved smt 0.4s (8%)

#59 L101:16:101:20 trivial tlapm

#70 L106:56:106:58 proved smt 0.1s (2%)

#71 L106:59:106:63 trivial tlapm

#72 L106:65:106:69 trivial tlapm

#138 L136:84:136:86 proved smt 0.1s (3%)

▶ <2>8 BY <2>8, <3>1, <2>3 37/37 tlapm

#118 L133:17:133:19 proved smt 0.6s (11%)

#119 L133:20:133:24 trivial tlapm

#120 L133:26:133:30 trivial tlapm

#121 L133:32:133:36 trivial tlapm

▶ <3>3 <3>3. currentTerm'[s1] = currentTerm[s1] 8/8 smt

#33 L88:11:88:13 proved smt 0.1s (2%)

#63 L103:28:103:30 proved smt 0.3s (5%)

#64 L103:31:103:47 trivial tlapm

#92 L115:55:115:57 proved smt 0.1s (2%)

#93 L115:58:115:62 trivial tlapm

#94 L115:64:115:68 trivial tlapm

#95 L115:70:115:74 trivial tlapm

#139 L138:84:138:86 proved smt 0.1s (3%)

▶ <3>1 BY <3>1, <2>4 25/25 tlapm

#1 L139:11:139:13 proved smt 0.9s (18%)

#2 L139:14:139:18 trivial tlapm

#3 L139:19:139:23 trivial tlapm

#4 L139:24:139:28 trivial tlapm

#5 L139:29:139:33 trivial tlapm

#6 L139:34:139:38 trivial tlapm

#7 L139:39:139:43 trivial tlapm

#19 L134:16:134:18 proved smt 0.2s (3%)

#20 L134:19:134:23 trivial tlapm

#21 L134:25:134:29 trivial tlapm

#22 L134:31:134:35 trivial tlapm

#23 L134:37:134:42 trivial tlapm

#24 L134:44:134:49 trivial tlapm

#25 L134:51:134:56 trivial tlapm

#40 L94:11:94:13 proved smt 0.4s (7%)

#41 L94:14:94:18 trivial tlapm

#54 L99:55:99:57 proved zenon 0.1s (1%)

#55 L99:58:99:62 trivial tlapm

#56 L99:64:99:68 trivial tlapm

#57 L99:70:99:74 trivial tlapm

#60 L102:69:102:71 proved smt 0.3s (7%)

#61 L102:72:102:76 trivial tlapm

#62 L102:78:102:82 trivial tlapm

#65 L104:41:104:43 proved smt 0.2s (4%)

#66 L104:44:104:48 trivial tlapm

THEOREM L_1 (H_OnePrimaryPerTerm)

Proof Tree