---

Step * 2 1 1 1 of Lemma consensus-refinement2


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)
BY
{ (Auto
   THEN (InstLemma `consensus-state2-cases` [⌈V⌉;⌈v⌉]⋅ THENA Auto)
   THEN D -1
   THEN ExRepD
   THEN SplitOrHyps
   THEN (HypSubst' -1 0 THENA Auto)) }

1
1. [V] : Type
2. v : consensus-state2(V)@i
3. v = AMBIVALENT ∈ 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)))))))^*) 
  AMBIVALENT

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

3
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]

---

Latex:



1.  [V]  :  Type
\mvdash{}  \mforall{}v:consensus-state2(V)
        (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)))))) 
          v)


By

(Auto
  THEN  (InstLemma  `consensus-state2-cases`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD
  THEN  SplitOrHyps
  THEN  (HypSubst'  -1  0  THENA  Auto))

---

Home Index