---

Step * 2 1 2 1 of Lemma consensus-refinement2

.....assertion..... 
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. cs-ref-map3(x) = PREDECIDED[v] ∈ consensus-state2(V)
⊢ (cs-ref-map3(y) = AMBIVALENT ∈ consensus-state2(V))
∨ (cs-ref-map3(y) = PREDECIDED[v] ∈ consensus-state2(V))
∨ (cs-ref-map3(y) = Decided[v] ∈ consensus-state2(V))
BY
{ ((RWO "cs-ref-map3-predecided<" (-1) THENA Auto)
   THEN (RWO "cs-ref-map3-decided<" 0⋅ THENA Auto)
   THEN (RWO "cs-ref-map3-predecided<" 0⋅ THENA Auto)) }

1
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. (∀v':V. (¬(COMMITED[v'] ∈ x))) ∧ (CONSIDERING[v] ∈ x)
⊢ (cs-ref-map3(y) = AMBIVALENT ∈ consensus-state2(V))
∨ ((∀v':V. (¬(COMMITED[v'] ∈ y))) ∧ (CONSIDERING[v] ∈ y))
∨ (COMMITED[v] ∈ y)

---

Latex:


.....assertion..... 
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.  cs-ref-map3(x)  =  PREDECIDED[v]
\mvdash{}  (cs-ref-map3(y)  =  AMBIVALENT)  \mvee{}  (cs-ref-map3(y)  =  PREDECIDED[v])  \mvee{}  (cs-ref-map3(y)  =  Decided[v])


By

((RWO  "cs-ref-map3-predecided<"  (-1)  THENA  Auto)
  THEN  (RWO  "cs-ref-map3-decided<"  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "cs-ref-map3-predecided<"  0\mcdot{}  THENA  Auto))

---

Home Index