---

Step * of Lemma cs-is-committed-implies

∀[V:Type]. ∀[x:consensus-state3(V)].
  x = COMMITED[cs-committed-val(x)] ∈ consensus-state3(V) supposing ↑cs-is-committed(x)
BY
{ (Unfolds ``consensus-state3 cs-is-committed cs-committed-val cs-commited`` 0 THEN Auto) }

1
1. V : Type
2. x : V + V + 𝔹
3. ↑isl(x)
⊢ x = (inl outl(x)) ∈ (V + V + 𝔹)

---

Latex:


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


By

(Unfolds  ``consensus-state3  cs-is-committed  cs-committed-val  cs-commited``  0  THEN  Auto)

---

Home Index