---

Step * 1 1 1 of Lemma cs-ref-map3_wf


1. V : Type
2. L : consensus-state3(V) List
3. v : {x:consensus-state3(V)| ↑((λx.cs-is-committed(x)) x)}  List@i
4. v1 : {x:consensus-state3(V)| ↑((λx.cs-is-considering(x)) x)}  List@i
⊢ let cmtd = v in
   let consd = v1 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)
BY
{ (All Reduce THEN RepUR ``let`` 0 THEN Auto) }

---

Latex:



1.  V  :  Type
2.  L  :  consensus-state3(V)  List
3.  v  :  \{x:consensus-state3(V)|  \muparrow{}((\mlambda{}x.cs-is-committed(x))  x)\}    List@i
4.  v1  :  \{x:consensus-state3(V)|  \muparrow{}((\mlambda{}x.cs-is-considering(x))  x)\}    List@i
\mvdash{}  let  cmtd  =  v  in
      let  consd  =  v1  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    \mmember{}  consensus-state2(V)


By

(All  Reduce  THEN  RepUR  ``let``  0  THEN  Auto)

---

Home Index