{ 
V:Type. A:Id List. t:
. f:V List 
V.
s:ts-reachable(three-consensus-ts(V;A;t;f)). a:{a:Id| (a 
A)} .
no_repeats(consensus-rcv(V;A);filter(
x.rcv-vote?(x);s a)) }
{ Proof }
Definitions occuring in Statement :
three-consensus-ts: three-consensus-ts(V;A;t;f),
rcv-vote?: rcv-vote?(x),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
nat_plus: ,
all: x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
list: type List,
universe: Type,
no_repeats: no_repeats(T;l),
filter: filter(P;l),
l_member: (x l),
ts-reachable: ts-reachable(ts)
Definitions :
so_lambda: 
x.t[x],
subtype: S 
T,
member: t T,
infix_ap: x f y,
prop: 
,
consensus-rcv: consensus-rcv(V;A),
ts-reachable: ts-reachable(ts),
all: x:A. B[x],
reduce: reduce(f;k;as),
pi2: snd(t),
pi1: fst(t),
three-consensus-ts: three-consensus-ts(V;A;t;f),
ts-init: ts-init(ts),
filter: filter(P;l),
implies: P 
Q,
top: Top,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
guard: {T},
and: P 
Q,
not: 
A,
ts-type: ts-type(ts),
so_apply: x[s],
sq_type: SQType(T),
unit: Unit,
rev_implies: P 
Q,
iff: P Q,
bool: 
,
false: False,
assert: 
b,
rcv-vote?: rcv-vote?(x),
it: 
,
cs-rcv-vote: Vote[a;i;v]
Lemmas :
Id_wf,
nat_plus_wf,
ts-init_wf,
ts-rel_wf,
rel_star_wf,
ts-type_wf,
rcv-vote?_wf,
assert_wf,
filter_type,
nat_wf,
no_repeats_wf,
l_member_wf,
nat_plus_inc,
three-consensus-ts_wf,
ts-reachable-induction,
ts-reachable_wf,
sq_stable__no_repeats,
filter_wf,
consensus-rcv_wf,
sq_stable__all,
no_repeats_nil,
Id_sq,
member_wf,
top_wf,
length_wf_nat,
l_disjoint_nil2,
l_disjoint_singleton,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
iff_transitivity,
no_repeats-single,
eqtt_to_assert,
bool_wf,
no_repeats-append,
filter_append_sq,
member_filter,
cs-rcv-vote_wf
\mforall{}V:Type. \mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:V List {}\mrightarrow{} V. \mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)).
\mforall{}a:\{a:Id| (a \mmember{} A)\} .
no\_repeats(consensus-rcv(V;A);filter(\mlambda{}x.rcv-vote?(x);s a))
Date html generated:
2011_08_16-AM-10_17_30
Last ObjectModification:
2011_01_03-PM-03_10_38
Home
Index