---

Step * of Lemma assert-cs-is-committed

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

1
1. [V] : Type
2. x : V + V + 𝔹@i
3. ↑isl(x)@i
⊢ ∃v:V. (x = (inl v) ∈ (V + V + 𝔹))

2
1. V : Type
2. x : V + V + 𝔹@i
3. ∃v:V. (x = (inl v) ∈ (V + V + 𝔹))@i
⊢ ↑isl(x)

---

Latex:


\mforall{}[V:Type].  \mforall{}x:consensus-state3(V).  (\muparrow{}cs-is-committed(x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}v:V.  (x  =  COMMITED[v]))


By

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

---

Home Index