{ 
[V:Type]. [A:Id List]. [L:consensus-rcv(V;A) List]. [i,n:
].
(filter(
r.i <z inning(r);L) ~ []) supposing
((n 
i) and
(filter(r.n <z inning(r);L) = [])) }
{ Proof }
Definitions occuring in Statement :
rcvd-inning-gt: i <z inning(r),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
uimplies: b supposing a,
uall: [x:A]. B[x],
le: A B,
lambda: x.A[x],
nil: [],
list: type List,
int: ,
universe: Type,
sqequal: s ~ t,
equal: s = t,
filter: filter(P;l)
Definitions :
l_all: (x
L.P[x]),
not: 
A,
so_apply: x[s],
member: t T,
all: x:A. B[x],
implies: P 
Q,
false: False,
prop: 
,
and: P 
Q,
rcvd-inning-gt: i <z inning(r),
assert: 
b,
band: p 
q,
rcv-vote?: rcv-vote?(x),
spreadn: spread3,
rcvd-vote: rcvd-vote(x),
bfalse: ff,
btrue: tt,
outr: outr(x),
ifthenelse: if b then t else f fi ,
top: Top,
subtype: S 
T,
uall: [x:A]. B[x],
uimplies: b supposing a,
iff: P 
Q,
rev_implies: P Q,
consensus-rcv: consensus-rcv(V;A),
le: A B,
nat: 
,
guard: {T}
Lemmas :
filter_is_nil,
rcvd-inning-gt_wf,
assert_wf,
l_member_wf,
le_wf,
consensus-rcv_wf,
filter_wf,
Id_wf,
member_filter,
false_wf,
lt_int_wf,
implies_functionality_wrt_iff,
iff_weakening_uiff,
assert_of_lt_int,
length_wf_nat,
filter_wf_top,
nat_wf,
top_wf,
member_wf,
nil_member
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[L:consensus-rcv(V;A) List]. \mforall{}[i,n:\mBbbZ{}].
(filter(\mlambda{}r.i <z inning(r);L) \msim{} []) supposing ((n \mleq{} i) and (filter(\mlambda{}r.n <z inning(r);L) = []))
Date html generated:
2011_08_16-AM-10_11_34
Last ObjectModification:
2011_06_18-AM-09_04_15
Home
Index