---

Step * 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
⊢ let cmtd = v 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)
BY
{ ((InstLemma `filter_type` [⌈consensus-state3(V)⌉;⌈λx.cs-is-considering(x)⌉;⌈L⌉]⋅ THENA Auto)
   THEN (GenConclAtAddr [2;2;1] THENA (Auto THEN Reduce 0 THEN Auto))
   THEN Thin (-3)
   THEN Thin (-1)) }

1
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)

---

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
\mvdash{}  let  cmtd  =  v  in
      let  consd  =  filter(\mlambda{}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    \mmember{}  consensus-state2(V)


By

((InstLemma  `filter\_type`  [\mkleeneopen{}consensus-state3(V)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.cs-is-considering(x)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddr  [2;2;1]  THENA  (Auto  THEN  Reduce  0  THEN  Auto))
  THEN  Thin  (-3)
  THEN  Thin  (-1))

---

Home Index