{ 
[V:Type]
((v,v':V. Dec(v = v'))
(A:Id List. W:{a:Id| (a 
A)} List List.
(one-intersection(A;W)
(s:ConsensusState. i:
.
L:V List
(v:V. in state s, inning i has committed v
(vL. in state s, inning i has committed v)))))) }
{ Proof }
Definitions occuring in Statement :
one-intersection: one-intersection(A;W),
cs-inning-committed: in state s, inning i has committed v,
consensus-state4: ConsensusState,
Id: Id,
decidable: Dec(P),
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
implies: P Q,
set: {x:A| B[x]} ,
list: type List,
int: ,
universe: Type,
equal: s = t,
l_exists: (xL. P[x]),
l_member: (x l)
Definitions :
true: True,
so_lambda: 
x.t[x],
prop: 
,
member: t T,
consensus-state4: ConsensusState,
all: x:A. B[x],
and: P 
Q,
uiff: uiff(P;Q),
so_apply: x[s],
uimplies: b supposing a,
uall: [x:A]. B[x],
l_all: (xL.P[x]),
implies: P Q,
one-intersection: one-intersection(A;W),
rev_implies: P Q,
iff: P Q,
cs-archived: by state s, a archived v in inning i,
fpf-domain: fpf-domain(f)
Lemmas :
fpf-ap_wf,
assert_wf,
subtype-top,
subtype-fpf2,
subtype_rel_simple_product,
subtype_rel_self,
fpf_wf,
subtype_rel_function,
top_wf,
cs-estimate_wf,
int-deq_wf,
fpf-dom_wf,
list-subtype,
l_member_wf,
Id_wf,
mapfilter_wf,
member-fpf-dom
\mforall{}[V:Type]
((\mforall{}v,v':V. Dec(v = v'))
{}\mRightarrow{} (\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List.
(one-intersection(A;W)
{}\mRightarrow{} (\mforall{}s:ConsensusState. \mforall{}i:\mBbbZ{}.
\mexists{}L:V List
(\mexists{}v:V. in state s, inning i has committed v
\mLeftarrow{}{}\mRightarrow{} (\mexists{}v\mmember{}L. in state s, inning i has committed v))))))
Date html generated:
2011_08_16-AM-10_01_42
Last ObjectModification:
2011_06_18-AM-09_00_12
Home
Index