---

Step * 2 1 2 2 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. cs-ref-map3(x) = PREDECIDED[v] ∈ consensus-state2(V)
9. (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))
⊢ PREDECIDED[v] (ts-rel(consensus-ts2(V))^*) cs-ref-map3(y)
BY
{ (RepUR ``ts-type ts-rel consensus-ts2`` 0
   THEN SplitOrHyps
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Auto
   THEN BLemma `rel_rel_star`
   THEN Auto
   THEN RepUR ``infix_ap`` 0
   THEN OrRight
   THEN Auto) }

---

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.  cs-ref-map3(x)  =  PREDECIDED[v]
9.  (cs-ref-map3(y)  =  AMBIVALENT)  \mvee{}  (cs-ref-map3(y)  =  PREDECIDED[v])  \mvee{}  (cs-ref-map3(y)  =  Decided[v])
\mvdash{}  PREDECIDED[v]  rel\_star(ts-type(consensus-ts2(V));  ts-rel(consensus-ts2(V)))  cs-ref-map3(y)


By

(RepUR  ``ts-type  ts-rel  consensus-ts2``  0
  THEN  SplitOrHyps
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  Auto
  THEN  BLemma  `rel\_rel\_star`
  THEN  Auto
  THEN  RepUR  ``infix\_ap``  0
  THEN  OrRight
  THEN  Auto)

---

Home Index