---

Step * of Lemma cs-is-considering-implies

∀[V:Type]. ∀[x:consensus-state3(V)].
  x = CONSIDERING[cs-considered-val(x)] ∈ consensus-state3(V) supposing ↑cs-is-considering(x)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN D -1
   THEN RepUR ``cs-is-considering cs-considered-val`` 0
   THEN Try (((D 0 THENM Trivial) THEN Auto))
   THEN D -1
   THEN Try (Fold `cs-considering` 0)
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[V:Type].  \mforall{}[x:consensus-state3(V)].
    x  =  CONSIDERING[cs-considered-val(x)]  supposing  \muparrow{}cs-is-considering(x)


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  RepUR  ``cs-is-considering  cs-considered-val``  0
  THEN  Try  (((D  0  THENM  Trivial)  THEN  Auto))
  THEN  D  -1
  THEN  Try  (Fold  `cs-considering`  0)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index