---

Step * of Lemma consensus-state2-cases

∀[V:Type]
  ∀x:consensus-state2(V)
    ((x = AMBIVALENT ∈ consensus-state2(V))
    ∨ (∃v:V. ((x = PREDECIDED[v] ∈ consensus-state2(V)) ∨ (x = Decided[v] ∈ consensus-state2(V)))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN D -1
   THEN Try ((Fold `cs-decided` 0⋅ THEN OrRight THEN Auto))
   THEN D -1
   THEN Try ((Fold `cs-predecided` 0 THEN OrRight THEN Auto))
   THEN Subst' (inr inr y1  ) = AMBIVALENT ∈ consensus-state2(V) 0
   THEN Auto) }

1
.....equality..... 
1. V : Type
2. y1 : Top@i
⊢ (inr inr y1  ) = AMBIVALENT ∈ consensus-state2(V)

---

Latex:


\mforall{}[V:Type]
    \mforall{}x:consensus-state2(V).  ((x  =  AMBIVALENT)  \mvee{}  (\mexists{}v:V.  ((x  =  PREDECIDED[v])  \mvee{}  (x  =  Decided[v]))))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  Try  ((Fold  `cs-decided`  0\mcdot{}  THEN  OrRight  THEN  Auto))
  THEN  D  -1
  THEN  Try  ((Fold  `cs-predecided`  0  THEN  OrRight  THEN  Auto))
  THEN  Subst'  (inr  inr  y1    )  =  AMBIVALENT  0
  THEN  Auto)

---

Home Index