---

Step * 2 1 1 1 3 of Lemma consensus-refinement2


1. [V] : Type
2. v : consensus-state2(V)@i
3. v@0 : V
4. v = Decided[v@0] ∈ 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)))))))^*) 
  Decided[v@0]
BY
{ ((Using [`y',⌈PREDECIDED[v@0]⌉] (BLemma `rel_star_transitivity`)⋅ THENA Auto) THEN BLemma `rel_rel_star` THEN Auto) }

1
1. [V] : Type
2. v : consensus-state2(V)@i
3. v@0 : V
4. v = Decided[v@0] ∈ 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))))))) 
  PREDECIDED[v@0]

2
1. [V] : Type
2. v : consensus-state2(V)@i
3. v@0 : V
4. v = Decided[v@0] ∈ consensus-state2(V)
⊢ PREDECIDED[v@0] 
  (λ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))))))) 
  Decided[v@0]

---

Latex:



1.  [V]  :  Type
2.  v  :  consensus-state2(V)@i
3.  v@0  :  V
4.  v  =  Decided[v@0]
\mvdash{}  AMBIVALENT 
    rel\_star(consensus-state2(V);
                      \mlambda{}x,y.  (((x  =  AMBIVALENT)  \mwedge{}  (\mexists{}v:V.  (y  =  PREDECIDED[v])))
                                \mvee{}  (\mexists{}v:V.  ((x  =  PREDECIDED[v])  \mwedge{}  ((y  =  Decided[v])  \mvee{}  (y  =  AMBIVALENT)))))) 
    Decided[v@0]


By

((Using  [`y',\mkleeneopen{}PREDECIDED[v@0]\mkleeneclose{}]  (BLemma  `rel\_star\_transitivity`)\mcdot{}  THENA  Auto)
  THEN  BLemma  `rel\_rel\_star`
  THEN  Auto)

---

Home Index