{ 
[V:Type]
A:Id List. W:{a:Id| (a 
A)} List List. v:V. i:
.
ts-stable(consensus-ts4(V;A;W);s.in state s, inning i has committed v) }
{ Proof }
Definitions occuring in Statement :
cs-inning-committed: in state s, inning i has committed v,
consensus-ts4: consensus-ts4(V;A;W),
Id: Id,
uall: [x:A]. B[x],
all: x:A. B[x],
set: {x:A| B[x]} ,
list: type List,
int: ,
universe: Type,
l_member: (x l),
ts-stable: ts-stable(ts;x.P[x])
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
ts-stable: ts-stable(ts;x.P[x]),
consensus-ts4: consensus-ts4(V;A;W),
cs-inning-committed: in state s, inning i has committed v,
ts-type: ts-type(ts),
implies: P 
Q,
infix_ap: x f y,
ts-rel: ts-rel(ts),
pi1: fst(t),
exists: 
x:A. B[x],
and: P 
Q,
pi2: snd(t),
member: t T,
prop: 
,
cand: A c B
Lemmas :
l_member_wf,
cs-archived_wf,
consensus-rel_wf,
cs-inning-committed_wf,
consensus-state4_wf,
ts-type_wf,
consensus-ts4_wf,
Id_wf,
consensus-ts4-archived-stable
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. \mforall{}v:V. \mforall{}i:\mBbbZ{}.
ts-stable(consensus-ts4(V;A;W);s.in state s, inning i has committed v)
Date html generated:
2011_08_16-AM-09_59_59
Last ObjectModification:
2011_06_18-AM-08_57_59
Home
Index