{ 
[V:Type]. 
[A:Id List]. 
[s:ConsensusState]. 
[a:{a:Id| (a 
 A)} ]. 
[i:
].
    (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, 
uall:
[x:A]. B[x], 
prop:
, 
member: t 
 T, 
set: {x:A| B[x]} , 
list: type List, 
int:
, 
universe: Type, 
l_member: (x 
 l)
Definitions : 
uall:
[x:A]. B[x], 
member: t 
 T, 
prop:
, 
cs-not-completed: in state s, a has not completed inning i, 
and: P 
 Q, 
cand: A c
 B, 
all:
x:A. B[x], 
so_lambda: 
x.t[x], 
true: True, 
uimplies: b supposing a, 
so_apply: x[s], 
uiff: uiff(P;Q)
Lemmas : 
le_wf, 
cs-inning_wf, 
not_wf, 
l_member_wf, 
fpf-domain_wf, 
cs-estimate_wf, 
subtype-fpf2, 
subtype-top, 
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{}].
    (in  state  s,  a  has  not  completed  inning  i  \mmember{}  \mBbbP{})
Date html generated:
2011_08_16-AM-09_58_46
Last ObjectModification:
2011_06_18-AM-08_57_15
Home
Index