{ 
[V:Type]. (consensus-ts3(V) 
transition-system{i:l}) }
{ Proof }
Definitions occuring in Statement :
consensus-ts3: consensus-ts3(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-ts3: consensus-ts3(T),
prop: 
,
infix_ap: x f y,
or: P 
Q,
and: P 
Q,
exists: 
x:A. B[x],
all: x:A. B[x],
implies: P 
Q,
not: 
A,
cand: A c B,
le: A 
B,
false: False,
int_seg: {i..j
},
lelt: i j < k,
uimplies: b supposing a
Lemmas :
consensus-state3_wf,
append_wf,
cs-initial_wf,
length_wf1,
int_seg_wf,
not_wf,
int_seg_properties,
select_wf,
cs-withdrawn_wf,
cs-considering_wf,
cs-commited_wf,
rel_star_wf
\mforall{}[V:Type]. (consensus-ts3(V) \mmember{} transition-system\{i:l\})
Date html generated:
2011_08_16-AM-09_56_16
Last ObjectModification:
2011_06_18-AM-08_56_03
Home
Index