Nuprl Lemma : consensus-refinement5
[V:Type]
A:Id List. W:{a:Id| (a 
A)} List List.
(((1 < ||W||) 
two-intersection(A;W))
ts-refinement(consensus-ts5(V;A;W);consensus-ts6(V;A;W);
s.cs-events-to-state(A; s)))
Proof not projected
Definitions occuring in Statement :
consensus-ts6: consensus-ts6(V;A;W),
cs-events-to-state: cs-events-to-state(A; s),
consensus-ts5: consensus-ts5(V;A;W),
two-intersection: two-intersection(A;W),
Id: Id,
length: ||as||,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
lambda: x.A[x],
list: type List,
natural_number: $n,
universe: Type,
l_member: (x l),
ts-refinement: ts-refinement(ts1;ts2;f)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
and: P Q,
ts-refinement: ts-refinement(ts1;ts2;f),
member: t T,
prop: 
,
so_lambda: 
x.t[x],
ycomb: Y,
list_accum: list_accum(x,a.f[x; a];y;l),
consensus-accum-state: consensus-accum-state(A;L),
spreadn: spread3,
pi2: snd(t),
top: Top,
bfalse: ff,
consensus-state5: Knowledge(ConsensusState),
consensus-state4: ConsensusState,
pi1: fst(t),
consensus-ts6: consensus-ts6(V;A;W),
cs-events-to-state: cs-events-to-state(A; s),
ts-init: ts-init(ts),
ts-rel: ts-rel(ts),
consensus-ts5: consensus-ts5(V;A;W),
ts-type: ts-type(ts),
infix_ap: x f y,
consensus-state6: consensus-state6(V;A),
exists: 
x:A. B[x],
consensus-rel-knowledge: consensus-rel-knowledge(V;A;W;x;y),
cs-inning: Inning(s;a),
cs-estimate: Estimate(s;a),
cs-knowledge: Knowledge(x;a),
or: 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),
subtype: S 
T,
so_lambda: x y.t[x; y],
cand: A c B,
not: 
A,
guard: {T},
false: False,
squash: 
T,
true: True,
so_apply: x[s],
ts-reachable: ts-reachable(ts),
reduce: reduce(f;k;as),
deq-member: deq-member(eq;x;L),
ifthenelse: if b then t else f fi ,
bnot: 
b,
assert: 
b,
btrue: tt,
eqof: eqof(d),
Id: Id,
one-consensus-event: y = x after e@a,
consensus-event-constraint: e@a allowed in state x,
outl: outl(x),
isl: isl(x),
outr: outr(x),
fpf-dom: x dom(f),
fpf-empty: 
,
cs-knowledge-precondition: may consider v in inning i based on knowledge (s),
fpf-domain: fpf-domain(f),
mk_fpf: mk_fpf(L;f),
le: A 
B,
bor: p q,
append: as @ bs,
ts-final: ts-final(ts),
iff: P 
Q,
rev_implies: P Q,
consensus-accum: consensus-accum(s;e),
archive-event: Archive(v),
fpf-cap: f(x)?z,
filter: filter(P;l),
fpf-join: f 
g,
fpf-single: x : v,
fpf: a:A fp-> B[a],
uimplies: b supposing a,
consensus-message: consensus-message(b;i;z),
inning-event: NextInning,
so_apply: x[s1;s2],
nat: 
,
int_seg: {i..j
},
lelt: i j < k,
unit: Unit,
decidable: Dec(P),
bool: 
,
sq_type: SQType(T),
consensus-event: consensus-event(V;A),
length: ||as||,
sq_stable: SqStable(P),
l_all: (xL.P[x]),
two-intersection: two-intersection(A;W),
uiff: uiff(P;Q),
it: 
,
eq_id: a = b
Lemmas :
and_wf,
less_than_wf,
length_wf,
Id_wf,
l_member_wf,
two-intersection_wf,
subtype_rel_simple_product,
consensus-rel-knowledge_wf,
mk_fpf_wf,
fpf-empty_wf,
top_wf,
fpf_wf,
rel_star_weakening,
consensus-event-cases,
rel_rel_star,
consensus-state4_wf,
consensus-state5_wf,
cs-events-to-state_wf,
pi1_wf_top,
consensus-accum-state_wf,
not_wf,
equal_wf,
length_wf_nat,
consensus-event_wf,
nat_wf,
member_wf,
append_wf,
list_accum_append,
list_accum_wf,
consensus-accum_wf,
pi2_wf,
consensus-rel-knowledge-step_wf,
cs-knowledge-precondition_wf,
fpf-join_wf,
fpf-single_wf,
int-deq_wf,
fpf-domain_wf,
fpf-trivial-subtype-top,
consensus-rel-add-knowledge-step_wf,
consensus-rel-knowledge-inning-step_wf,
consensus-rel-knowledge-archive-step_wf,
ts-rel_wf,
consensus-ts6_wf,
ts-reachable_wf,
ts-type_wf,
or_wf,
int_seg_properties,
assert_witness,
fpf-dom_wf,
assert_wf,
all_wf,
pair_wf,
fpf-ap_wf,
id-deq_wf,
le_wf,
squash_wf,
true_wf,
deq_wf,
nat_properties,
consensus-ts5_wf,
ts-final_wf,
ts-init_wf,
rel_star_wf,
archive-event_wf,
decidable__equal_Id,
decidable__l_member,
eqof_wf,
bor_wf,
deq-member_wf,
ifthenelse_wf,
rel_star_transitivity,
not_functionality_wrt_uiff,
and_functionality_wrt_uiff2,
assert_of_band,
bnot_thru_bor,
assert_functionality_wrt_uiff,
uiff_transitivity,
assert-eq-id,
or_functionality_wrt_uiff2,
assert_of_bor,
not_functionality_wrt_iff,
assert_of_bnot,
eqff_to_assert,
assert-deq-member,
eqtt_to_assert,
iff_weakening_uiff,
iff_transitivity,
bfalse_wf,
false_wf,
bnot_wf,
band_wf,
btrue_wf,
eq_id_wf,
bool_wf,
strong-subtype-self,
strong-subtype-set3,
strong-subtype-deq-subtype,
l_member_set2,
atom2_subtype_base,
subtype_base_sq,
exists_wf,
one-consensus-event_wf,
consensus-event-constraint_wf,
unit_wf2,
int_seg_wf,
consensus-message_wf,
outl_wf,
isl_wf,
outr_wf,
unit_wf,
nil_member,
sq_stable_from_decidable,
property-from-l_member,
cons_member,
sq_stable__assert,
list-subtype,
l_member-set,
pair_eta_rw
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List.
(((1 < ||W||) \mwedge{} two-intersection(A;W))
{}\mRightarrow{} ts-refinement(consensus-ts5(V;A;W);consensus-ts6(V;A;W);\mlambda{}s.cs-events-to-state(A; s)))
Date html generated:
2012_01_23-PM-12_07_05
Last ObjectModification:
2011_12_31-AM-11_10_16
Home
Index