{ [V:Type]. [v:V].  (Decided[v]  consensus-state2(V)) }

{ Proof }



Definitions occuring in Statement :  consensus-state2: consensus-state2(T) cs-decided: Decided[v] uall: [x:A]. B[x] member: t  T universe: Type
Definitions :  uall: [x:A]. B[x] member: t  T consensus-state2: consensus-state2(T) cs-decided: Decided[v]
Lemmas :  top_wf

\mforall{}[V:Type].  \mforall{}[v:V].    (Decided[v]  \mmember{}  consensus-state2(V))


Date html generated: 2011_08_16-AM-09_54_25
Last ObjectModification: 2011_06_18-AM-08_36_43

Home Index