{ 
[V:Type]. (consensus-ts1(V) 
transition-system{i:l}) }
{ Proof }
Definitions occuring in Statement :
consensus-ts1: consensus-ts1(T),
uall: [x:A]. B[x],
member: t T,
universe: Type,
transition-system: transition-system{i:l}
Definitions :
uall: [x:A]. B[x],
member: t T,
transition-system: transition-system{i:l},
consensus-ts1: consensus-ts1(T),
prop: 
,
infix_ap: x f y,
and: P 
Q,
exists: 
x:A. B[x]
Lemmas :
consensus-state1_wf,
cs-undecided_wf,
cs-decided_wf,
rel_star_wf
\mforall{}[V:Type]. (consensus-ts1(V) \mmember{} transition-system\{i:l\})
Date html generated:
2011_08_16-AM-09_54_20
Last ObjectModification:
2011_06_18-AM-08_36_35
Home
Index