---

Step * of Lemma cs-ref-map3_wf

∀[V:Type]. ∀[L:consensus-state3(V) List].  (cs-ref-map3(L) ∈ consensus-state2(V))
BY
{ (Auto THEN Unfold `cs-ref-map3` 0) }

1
1. V : Type
2. L : consensus-state3(V) List
⊢ let cmtd = filter(λx.cs-is-committed(x);L) in
   let consd = filter(λx.cs-is-considering(x);L) in
   if null(cmtd)
   then if null(consd) then AMBIVALENT else PREDECIDED[cs-considered-val(hd(consd))] fi 
   else Decided[cs-committed-val(hd(cmtd))]
   fi  ∈ consensus-state2(V)

---

Latex:

---

Latex:
\mforall{}[V:Type].  \mforall{}[L:consensus-state3(V)  List].    (cs-ref-map3(L)  \mmember{}  consensus-state2(V))


By

---

Latex:
(Auto  THEN  Unfold  `cs-ref-map3`  0)

---

Home Index