---

Step * 2 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. x ts-rel(consensus-ts3(V)) y@i
5. x ∈ consensus-state3(V) List
6. y ∈ consensus-state3(V) List
7. cs-ref-map3(x) = AMBIVALENT ∈ consensus-state2(V)
⊢ AMBIVALENT (ts-rel(consensus-ts2(V))^*) cs-ref-map3(y)
BY
{ ((GenConclAtAddr [3] THEN Auto) THEN RepUR ``ts-rel ts-type consensus-ts2`` 0 THEN Lemmaize []) }

1
1. [V] : Type
⊢ ∀v:consensus-state2(V)
    (AMBIVALENT 
     ((λx,y. (((x = AMBIVALENT ∈ consensus-state2(V)) ∧ (∃v:V. (y = PREDECIDED[v] ∈ consensus-state2(V))))
            ∨ (∃v:V
                ((x = PREDECIDED[v] ∈ consensus-state2(V))
                ∧ ((y = Decided[v] ∈ consensus-state2(V)) ∨ (y = AMBIVALENT ∈ consensus-state2(V)))))))^*) 
     v)

---

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


By

((GenConclAtAddr  [3]  THEN  Auto)  THEN  RepUR  ``ts-rel  ts-type  consensus-ts2``  0  THEN  Lemmaize  [])

---

Home Index