Nuprl Lemma : cs-possible-state-reachable
[V:Type]. [A:Id List]. [W:{a:Id| (a 
A)} List List]. [v:V].
([L:{a:Id| (a A)} List]
(<
a.<0, if deq-member(IdDeq;a;L) then 0 : v else 
fi >, a.mk_fpf(A;b.<0, ff>)>
ts-reachable(consensus-ts5(V;A;W)))) supposing
(two-intersection(A;W) and
(1 < ||W||))
Proof not projected
Definitions occuring in Statement :
consensus-ts5: consensus-ts5(V;A;W),
two-intersection: two-intersection(A;W),
mk_fpf: mk_fpf(L;f),
fpf-single: x : v,
fpf-empty: ,
id-deq: IdDeq,
Id: Id,
length: ||as||,
ifthenelse: if b then t else f fi ,
bfalse: ff,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
less_than: a < b,
set: {x:A| B[x]} ,
lambda: x.A[x],
pair: <a, b>,
list: type List,
natural_number: $n,
universe: Type,
l_member: (x l),
deq-member: deq-member(eq;x;L),
ts-reachable: ts-reachable(ts)
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t T,
ts-reachable: ts-reachable(ts),
consensus-ts5: consensus-ts5(V;A;W),
bfalse: ff,
ts-type: ts-type(ts),
consensus-state4: ConsensusState,
consensus-state5: Knowledge(ConsensusState),
all: x:A. B[x],
pi1: fst(t),
top: Top,
pi2: snd(t),
infix_ap: x f y,
ts-rel: ts-rel(ts),
ts-init: ts-init(ts),
prop: 
,
so_lambda: 
x.t[x],
squash: 
T,
true: True,
subtype: S 
T,
ifthenelse: if b then t else f fi ,
implies: P 
Q,
btrue: tt,
deq-member: deq-member(eq;x;L),
reduce: reduce(f;k;as),
eqof: eqof(d),
and: P 
Q,
cand: A c B,
assert: 
b,
guard: {T},
bnot: 
b,
consensus-rel-knowledge: consensus-rel-knowledge(V;A;W;x;y),
exists: 
x:A. B[x],
consensus-rel-knowledge-step: consensus-rel-knowledge-step(V;A;W;x1;x2;y1;y2;a),
cs-inning: Inning(s;a),
bor: p 
q,
cs-estimate: Estimate(s;a),
or: P Q,
consensus-rel-knowledge-archive-step: consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a),
cs-knowledge: Knowledge(x;a),
fpf-single: x : v,
fpf-empty: ,
fpf-domain: fpf-domain(f),
exposed-bfalse: exposed-bfalse,
not: A,
cs-knowledge-precondition: may consider v in inning i based on knowledge (s),
isl: isl(x),
false: False,
mk_fpf: mk_fpf(L;f),
fpf-dom: x dom(f),
so_apply: x[s],
iff: P 
Q,
bool: 
,
unit: Unit,
decidable: Dec(P),
uiff: uiff(P;Q),
rev_implies: P Q,
length: ||as||,
ycomb: Y,
sq_stable: SqStable(P),
two-intersection: two-intersection(A;W),
l_all: (xL.P[x]),
it: 
,
eq_id: a = b
Lemmas :
l_member_wf,
ifthenelse_wf,
deq-member_wf,
Id_wf,
id-deq_wf,
fpf_wf,
fpf-single_wf,
fpf-empty_wf,
mk_fpf_wf,
top_wf,
rel_star_wf,
consensus-rel-knowledge_wf,
subtype_rel_simple_product,
two-intersection_wf,
less_than_wf,
length_wf,
rel_star_weakening,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
bool_wf,
equal_wf,
assert_wf,
nil_member,
bnot_wf,
not_wf,
iff_transitivity,
iff_weakening_uiff,
eqtt_to_assert,
assert-deq-member,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_iff,
rel_star_transitivity,
rel_rel_star,
decidable__l_member,
decidable__equal_set,
decidable__equal_Id,
bor_wf,
eq_id_wf,
btrue_wf,
or_wf,
true_wf,
band_wf,
false_wf,
bfalse_wf,
member_wf,
assert_of_bor,
or_functionality_wrt_uiff2,
assert-eq-id,
uiff_transitivity,
assert_functionality_wrt_uiff,
bnot_thru_bor,
assert_of_band,
and_functionality_wrt_uiff2,
not_functionality_wrt_uiff,
squash_wf,
consensus-rel-knowledge-step_wf,
eqof_wf,
cs-knowledge_wf,
consensus-rel-add-knowledge-step_wf,
consensus-rel-knowledge-inning-step_wf,
l_member_set2,
cs-knowledge-precondition_wf,
fpf-join_wf,
int-deq_wf,
all_wf,
fpf-dom_wf,
exists_wf,
cons_member,
sq_stable__assert,
fpf-join-empty
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[W:\{a:Id| (a \mmember{} A)\} List List]. \mforall{}[v:V].
(\mforall{}[L:\{a:Id| (a \mmember{} A)\} List]
(<\mlambda{}a.ɘ, if deq-member(IdDeq;a;L) then 0 : v else \motimes{} fi >, \mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ, ff>)>
\mmember{} ts-reachable(consensus-ts5(V;A;W)))) supposing
(two-intersection(A;W) and
(1 < ||W||))
Date html generated:
2012_01_23-PM-12_06_32
Last ObjectModification:
2011_12_19-PM-04_32_37
Home
Index