{ 
[V:Type]
A:Id List. s:ConsensusState. a:{a:Id| (a 
A)} . i:
.
Dec(in state s, a has not completed inning i) }
{ Proof }
Definitions occuring in Statement :
cs-not-completed: in state s, a has not completed inning i,
consensus-state4: ConsensusState,
Id: Id,
decidable: Dec(P),
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)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
cs-not-completed: in state s, a has not completed inning i,
prop: 
,
member: t T,
so_lambda: 
x.t[x],
true: True,
and: P 
Q,
implies: P 
Q,
uimplies: b supposing a,
so_apply: x[s],
uiff: uiff(P;Q)
Lemmas :
decidable__and,
le_wf,
cs-inning_wf,
not_wf,
l_member_wf,
fpf-domain_wf,
cs-estimate_wf,
subtype-fpf2,
subtype-top,
decidable__le,
decidable__not,
decidable__l_member,
decidable__equal_int,
Id_wf,
consensus-state4_wf
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}s:ConsensusState. \mforall{}a:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbZ{}.
Dec(in state s, a has not completed inning i)
Date html generated:
2011_08_16-AM-09_58_50
Last ObjectModification:
2011_06_18-AM-08_57_19
Home
Index