{ 
[V:Type]
((v1,v2:V. Dec(v1 = v2))
(
v,v':V. (
(v = v')))
(A:Id List. W:{a:Id| (a 
A)} List List.
x:ts-reachable(consensus-ts5(V;A;W)). v:V. b:{a:Id| (a A)} . i:
.
(state fst(x) may consider v in inning i) supposing
((Estimate(fst(x);b)(i) = v) and
(
i dom(Estimate(fst(x);b)))))) }
{ Proof }
Definitions occuring in Statement :
consensus-ts5: consensus-ts5(V;A;W),
cs-precondition: state s may consider v in inning i,
cs-estimate: Estimate(s;a),
fpf-ap: f(x),
fpf-dom: x dom(f),
Id: Id,
assert: b,
decidable: Dec(P),
uimplies: b supposing a,
uall: [x:A]. B[x],
pi1: fst(t),
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
set: {x:A| B[x]} ,
list: type List,
int: ,
universe: Type,
equal: s = t,
l_member: (x l),
int-deq: IntDeq,
ts-reachable: ts-reachable(ts)
Definitions :
all: x:A. B[x],
uimplies: b supposing a,
pi1: fst(t),
consensus-state4: ConsensusState,
uall: [x:A]. B[x],
prop: 
,
member: t T,
so_lambda: 
x.t[x],
true: True,
assert: b,
fpf-dom: x dom(f),
cs-estimate: Estimate(s;a),
ts-init: ts-init(ts),
consensus-ts5: consensus-ts5(V;A;W),
pi2: snd(t),
fpf-empty: 
,
bfalse: ff,
deq-member: deq-member(eq;x;L),
reduce: reduce(f;k;as),
ifthenelse: if b then t else f fi ,
false: False,
exists: x:A. B[x],
implies: P Q,
infix_ap: x f y,
ts-rel: ts-rel(ts),
consensus-rel-knowledge: consensus-rel-knowledge(V;A;W;x;y),
top: Top,
cs-precondition: state s may consider v in inning i,
and: P 
Q,
cand: A c B,
btrue: tt,
squash: 
T,
so_apply: x[s],
not: A,
cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i,
ts-type: ts-type(ts),
ts-reachable: ts-reachable(ts),
le: A 
B,
Id: Id,
or: P 
Q,
uiff: uiff(P;Q),
consensus-rel-knowledge-step: consensus-rel-knowledge-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-knowledge-inning-step: consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-knowledge-archive-step: consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-add-knowledge-step: consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a),
decidable: Dec(P),
guard: {T},
sq_type: SQType(T),
cs-knowledge-precondition: may consider v in inning i based on knowledge (s),
iff: P 
Q,
rev_implies: P Q
Lemmas :
sq_stable__all,
assert_wf,
fpf-dom_wf,
cs-estimate_wf,
subtype_rel_function,
Id_wf,
l_member_wf,
fpf_wf,
top_wf,
subtype_rel_self,
subtype_rel_simple_product,
subtype-fpf2,
subtype-top,
sq_stable__uall,
assert_witness,
sq_stable_from_decidable,
cs-precondition_wf,
decidable__cs-precondition,
ts-reachable_wf,
consensus-ts5_wf,
ts-type_wf,
false_wf,
fpf-ap_wf,
int-deq_wf,
consensus-rel-knowledge-step_wf,
pi1_wf_top,
consensus-state4_wf,
pi2_wf,
consensus-state5_wf,
decidable__equal_Id,
le_wf,
cs-inning_wf,
not_wf,
cs-archive-blocked_wf,
member_wf,
fpf-trivial-subtype-top,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_elim,
squash_wf,
true_wf,
deq_wf,
fpf-join_wf,
fpf-single_wf,
cs-knowledge-precondition_wf,
decidable__equal_int,
int_subtype_base,
rel_star_wf,
ts-rel_wf,
ts-init_wf,
consensus-ts5-true-knowledge,
id-deq_wf,
atom2_subtype_base,
fpf-join-single-property,
fpf-join-dom,
bnot_wf,
fpf-join-ap-sq,
bool_cases,
iff_weakening_uiff,
eqtt_to_assert,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot
\mforall{}[V:Type]
((\mforall{}v1,v2:V. Dec(v1 = v2))
{}\mRightarrow{} (\mexists{}v,v':V. (\mneg{}(v = v')))
{}\mRightarrow{} (\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. \mforall{}x:ts-reachable(consensus-ts5(V;A;W)). \mforall{}v:V.
\mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbZ{}.
(state fst(x) may consider v in inning i) supposing
((Estimate(fst(x);b)(i) = v) and
(\muparrow{}i \mmember{} dom(Estimate(fst(x);b))))))
Date html generated:
2011_08_16-AM-10_08_32
Last ObjectModification:
2011_06_18-AM-09_02_07
Home
Index