{ 
[V:Type]. (consensus-ts2(V) 
transition-system{i:l}) }
{ Proof }
Definitions occuring in Statement :
consensus-ts2: consensus-ts2(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-ts2: consensus-ts2(T),
prop: 
,
infix_ap: x f y,
or: P 
Q,
and: P 
Q,
exists: 
x:A. B[x],
all: x:A. B[x]
Lemmas :
consensus-state2_wf,
cs-ambivalent_wf,
cs-predecided_wf,
cs-decided_wf2,
rel_star_wf
\mforall{}[V:Type]. (consensus-ts2(V) \mmember{} transition-system\{i:l\})
Date html generated:
2011_08_16-AM-09_54_47
Last ObjectModification:
2011_06_18-AM-08_54_40
Home
Index