---

Step * 2 1 3 1 of Lemma consensus-refinement2


1. V : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. x ts-rel(consensus-ts3(V)) y@i
5. x ∈ consensus-state3(V) List
6. y ∈ consensus-state3(V) List
7. v : V
8. (COMMITED[v] ∈ x)
⊢ (COMMITED[v] ∈ y)
BY
{ ((InstLemma `consensus-ts3-invariant1` [⌈V⌉;⌈x⌉;⌈v⌉]⋅ THENA Auto)
   THEN RepUR ``ts-rel consensus-ts3 infix_ap`` 4
   THEN RepeatFor 3 ((SplitOrHyps THEN ExRepD))) }

1
1. V : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. y = (x @ [INITIAL]) ∈ (consensus-state3(V) List)@i
5. x ∈ consensus-state3(V) List
6. y ∈ consensus-state3(V) List
7. v : V
8. (COMMITED[v] ∈ x)
9. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
⊢ (COMMITED[v] ∈ y)

2
1. V : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. ||y|| = ||x|| ∈ ℤ@i
5. i : ℕ||x||@i
6. ∀j:ℕ||x||. ((¬(j = i ∈ ℤ)) ⇒ (y[j] = x[j] ∈ consensus-state3(V)))@i
7. x[i] = INITIAL ∈ consensus-state3(V)@i
8. y[i] = WITHDRAWN ∈ consensus-state3(V)@i
9. x ∈ consensus-state3(V) List
10. y ∈ consensus-state3(V) List
11. v : V
12. (COMMITED[v] ∈ x)
13. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
⊢ (COMMITED[v] ∈ y)

3
1. V : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. ||y|| = ||x|| ∈ ℤ@i
5. i : ℕ||x||@i
6. ∀j:ℕ||x||. ((¬(j = i ∈ ℤ)) ⇒ (y[j] = x[j] ∈ consensus-state3(V)))@i
7. x[i] = INITIAL ∈ consensus-state3(V)@i
8. v1 : V@i
9. y[i] = CONSIDERING[v1] ∈ consensus-state3(V)@i
10. ∀j:ℕi
      ((x[j] = WITHDRAWN ∈ consensus-state3(V))
      ∨ (x[j] = CONSIDERING[v1] ∈ consensus-state3(V))
      ∨ (x[j] = COMMITED[v1] ∈ consensus-state3(V)))@i
11. x ∈ consensus-state3(V) List
12. y ∈ consensus-state3(V) List
13. v : V
14. (COMMITED[v] ∈ x)
15. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
⊢ (COMMITED[v] ∈ y)

4
1. V : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. ||y|| = ||x|| ∈ ℤ@i
5. i : ℕ||x||@i
6. ∀j:ℕ||x||. ((¬(j = i ∈ ℤ)) ⇒ (y[j] = x[j] ∈ consensus-state3(V)))@i
7. v1 : V@i
8. x[i] = CONSIDERING[v1] ∈ consensus-state3(V)@i
9. y[i] = COMMITED[v1] ∈ consensus-state3(V)@i
10. x ∈ consensus-state3(V) List
11. y ∈ consensus-state3(V) List
12. v : V
13. (COMMITED[v] ∈ x)
14. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
⊢ (COMMITED[v] ∈ y)

5
1. V : Type
2. x : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. ||y|| = ||x|| ∈ ℤ@i
5. i : ℕ||x||@i
6. ∀j:ℕ||x||. ((¬(j = i ∈ ℤ)) ⇒ (y[j] = x[j] ∈ consensus-state3(V)))@i
7. v1 : V@i
8. x[i] = CONSIDERING[v1] ∈ consensus-state3(V)@i
9. y[i] = WITHDRAWN ∈ consensus-state3(V)@i
10. x ∈ consensus-state3(V) List
11. y ∈ consensus-state3(V) List
12. v : V
13. (COMMITED[v] ∈ x)
14. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
⊢ (COMMITED[v] ∈ y)

---

Latex:



1.  V  :  Type
2.  x  :  ts-reachable(consensus-ts3(V))@i
3.  y  :  ts-reachable(consensus-ts3(V))@i
4.  x  ts-rel(consensus-ts3(V))  y@i
5.  x  \mmember{}  consensus-state3(V)  List
6.  y  \mmember{}  consensus-state3(V)  List
7.  v  :  V
8.  (COMMITED[v]  \mmember{}  x)
\mvdash{}  (COMMITED[v]  \mmember{}  y)


By

((InstLemma  `consensus-ts3-invariant1`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``ts-rel  consensus-ts3  infix\_ap``  4
  THEN  RepeatFor  3  ((SplitOrHyps  THEN  ExRepD)))

---

Home Index