{ 
[V:Type]. [A:Id List]. [t:
]. [f:V List 
V].
(three-consensus-ts(V;A;t;f) 
transition-system{i:l}) }
{ Proof }
Definitions occuring in Statement :
three-consensus-ts: three-consensus-ts(V;A;t;f),
Id: Id,
nat: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
list: type List,
universe: Type,
transition-system: transition-system{i:l}
Definitions :
uall: [x:A]. B[x],
member: t T,
transition-system: transition-system{i:l},
three-consensus-ts: three-consensus-ts(V;A;t;f),
prop: 
,
infix_ap: x f y,
exists: 
x:A. B[x],
and: P 
Q,
all: x:A. B[x],
implies: P 
Q,
nat:
Lemmas :
Id_wf,
l_member_wf,
consensus-rcv_wf,
nat_wf,
cs-rcv-vote_wf,
iseg_wf,
archive-condition_wf,
not_wf,
append_wf,
cs-initial-rcv_wf,
rel_star_wf
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}]. \mforall{}[f:V List {}\mrightarrow{} V].
(three-consensus-ts(V;A;t;f) \mmember{} transition-system\{i:l\})
Date html generated:
2011_08_16-AM-10_16_47
Last ObjectModification:
2011_06_18-AM-09_06_49
Home
Index