{ 
[V:Type]. (UNDECIDED 
consensus-state1(V)) }
{ Proof }
Definitions occuring in Statement :
cs-undecided: UNDECIDED,
consensus-state1: consensus-state1(V),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
consensus-state1: consensus-state1(V),
cs-undecided: UNDECIDED,
top: Top
Lemmas :
it_wf,
unit_wf
\mforall{}[V:Type]. (UNDECIDED \mmember{} consensus-state1(V))
Date html generated:
2011_08_16-AM-09_54_13
Last ObjectModification:
2011_06_18-AM-08_36_27
Home
Index