---

Step * 2 1 2 1 1 1 1 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. y = (x @ [INITIAL]) ∈ (consensus-state3(V) List)@i
5. x ∈ consensus-state3(V) List
6. y ∈ consensus-state3(V) List
7. v : V
8. ∀v':V. (¬(COMMITED[v'] ∈ x))
9. (CONSIDERING[v] ∈ x)
10. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
11. v' : V@i
⊢ ¬((COMMITED[v'] ∈ x) ∨ (COMMITED[v'] = INITIAL ∈ consensus-state3(V)))
BY
{ ((D 0 THEN Auto) THEN D -1 THEN Auto) }

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. ∀v':V. (¬(COMMITED[v'] ∈ x))
9. (CONSIDERING[v] ∈ x)
10. ∀[v':V]. v' = v ∈ V supposing (CONSIDERING[v'] ∈ x) ∨ (COMMITED[v'] ∈ x)
11. v' : V@i
12. COMMITED[v'] = INITIAL ∈ consensus-state3(V)@i
⊢ False

---

Latex:



1.  V  :  Type
2.  x  :  ts-reachable(consensus-ts3(V))@i
3.  y  :  ts-reachable(consensus-ts3(V))@i
4.  y  =  (x  @  [INITIAL])@i
5.  x  \mmember{}  consensus-state3(V)  List
6.  y  \mmember{}  consensus-state3(V)  List
7.  v  :  V
8.  \mforall{}v':V.  (\mneg{}(COMMITED[v']  \mmember{}  x))
9.  (CONSIDERING[v]  \mmember{}  x)
10.  \mforall{}[v':V].  v'  =  v  supposing  (CONSIDERING[v']  \mmember{}  x)  \mvee{}  (COMMITED[v']  \mmember{}  x)
11.  v'  :  V@i
\mvdash{}  \mneg{}((COMMITED[v']  \mmember{}  x)  \mvee{}  (COMMITED[v']  =  INITIAL))


By

((D  0  THEN  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index