Nuprl Lemma : implies-is-threshold1

{

[Info:Type].

[es:EO+(Info)].

[A:Type].

[X:EClass(A)].

[S:Type].

[init:S].

[f:S

A

S].

[test:S

A

].

[nxt:S

A

S].

[e:E].
((

[e':E(Threshold(init;f;test;nxt;X))]
((

e

prior(Threshold(init;f;test;nxt;X)))

(prior(Threshold(init;f;test;nxt;X))(e) = e'))

(

e

Threshold(init;f;test;nxt;X)) supposing
((

(test
                 list_accum(s,v.f s v;
                            nxt Threshold(init;f;test;nxt;X)(e');
                            X(e', e))
                 X(e))) and
             (

e

X))
supposing (e' <loc e)

(

e'':E(X)
((e' <loc e'')

(e'' <loc e)

(

(test
                    list_accum(s,v.f s v;
                               nxt Threshold(init;f;test;nxt;X)(e');
                               X(e', e''))
                    X(e''))))))

(

e

prior(Threshold(init;f;test;nxt;X)))

(

e

Threshold(init;f;test;nxt;X)) supposing
((

(test list_accum(s,v.f s v;init;X(<e)) X(e))) and
(

e

X))
supposing

e':E(X)
((e' <loc e)

(

(test list_accum(s,v.f s v;init;X(<e')) X(e'))))) }

{ Proof }

Definitions occuring in Statement : es-threshold: Threshold(init;f;test;nxt;X), es-prior-interface: prior(X), es-prior-interval-vals: X(e1, e2), es-prior-interface-vals: X(<e), es-E-interface: E(X), eclass-val: X(e), in-eclass: e

X, eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-locl: (e <loc e'), es-E: E, assert:

b, bool:

, uimplies: b supposing a, uall:

[x:A]. B[x], all:

x:A. B[x], not:

A, implies: P

Q, and: P

Q, apply: f a, function: x:A

B[x], product: x:A

B[x], universe: Type, equal: s = t, list_accum: list_accum(x,a.f[x; a];y;l)
Definitions : bfalse: ff, isl: isl(x), can-apply: can-apply(f;x), let: let, es-rec-class: es-rec-class, cond-class: [X?Y], es-loc: loc(e), exists:

x:A. B[x], es-interface-at: X@i, intensional-universe: IType, tag-by: z

T, rev_implies: P

Q, iff: P

Q, fset: FSet{T}, isect2: T1

T2, b-union: A

B, bag: bag(T), list: type List, fpf-cap: f(x)?z, record: record(x.T[x]), Id: Id, is_list_splitting: is_list_splitting(T;L;LL;L2;f), is_accum_splitting: is_accum_splitting(T;A;L;LL;L2;f;g;x), req: x = y, rnonneg: rnonneg(r), rleq: x

y, i-member: r

I, partitions: partitions(I;p), modulus-of-ccontinuity: modulus-of-ccontinuity(omega;I;f), fpf-sub: f

g, squash:

T, sq_stable: SqStable(P), es-local-pred: last(P), so_apply: x[s], or: P

Q, eq_knd: a = b, l_member: (x

l), fpf-dom: x

dom(f), so_lambda:

x.t[x], cand: A c

B, es-prior-interface-vals: X(<e), null: null(as), guard: {T}, sq_type: SQType(T), btrue: tt, es-prior-interval-vals: X(e1, e2), list_accum: list_accum(x,a.f[x; a];y;l), fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), infix_ap: x f y, es-causl: (e < e'), set: {x:A| B[x]} , le: A

B, ge: i

j , less_than: a < b, uiff: uiff(P;Q), in-eclass: e

X, axiom: Ax, es-prior-interface: prior(X), eclass-val: X(e), prop:

, es-locl: (e <loc e'), es-threshold: Threshold(init;f;test;nxt;X), es-E-interface: E(X), pair: <a, b>, implies: P

Q, not:

A, void: Void, false: False, true: True, decide: case b of inl(x) => s[x] | inr(y) => t[y], assert:

b, uimplies: b supposing a, and: P

Q, product: x:A

B[x], bool:

, union: left + right, subtype: S

T, subtype_rel: A

r B, atom: Atom, apply: f a, top: Top, es-base-E: es-base-E(es), token: "$token", ifthenelse: if b then t else f fi , record-select: r.x, event_ordering: EO, es-E: E, lambda:

x.A[x], so_lambda:

x y.t[x; y], eclass: EClass(A[eo; e]), dep-isect: Error :dep-isect, eq_atom: x =a y, eq_atom: eq_atom$n(x;y), record+: record+, all:

x:A. B[x], function: x:A

B[x], isect:

x:A. B[x], uall:

[x:A]. B[x], universe: Type, member: t

T, event-ordering+: EO+(Info), equal: s = t, tactic: Error :tactic, limited-type: LimitedType, real:

, grp_car: |g|, minus: -n, add: n + m, subtract: n - m, natural_number: $n, int:

, nat:

, strongwellfounded: SWellFounded(R[x; y]), MaAuto: Error :MaAuto, CollapseTHEN: Error :CollapseTHEN, Auto: Error :Auto, D: Error :D, CollapseTHENA: Error :CollapseTHENA, RepeatFor: Error :RepeatFor, it:

, map-class: (f[v] where v from X), es-filter-image: f[X], imax-class: (maximum f[v]

lb with v from X), es-le: e

loc e' , unit: Unit, bnot:

b, bor: p

q, band: p

q, bimplies: p

q, es-eq-E: e = e', eq_lnk: a = b, eq_id: a = b, eq_str: Error :eq_str, deq-all-disjoint: deq-all-disjoint(eq;ass;bs), deq-disjoint: deq-disjoint(eq;as;bs), deq-member: deq-member(eq;x;L), q_le: q_le(r;s), q_less: q_less(r;s), qeq: qeq(r;s), eq_type: eq_type(T;T'), b-exists: (

i<n.P[i])_b, bl-exists: (

x

L.P[x])_b, bl-all: (

x

L.P[x])_b, dcdr-to-bool: [d]

, grp_blt: a <

b, set_blt: a <

b, eq_int: (i =

j), le_int: i

z j, lt_int: i <z j, eq_bool: p =b q, sqequal: s ~ t
Lemmas : es-is-prior-interface, squash_wf, set_subtype_base, unit_wf, bnot_wf, assert_of_bnot, eqff_to_assert, uiff_transitivity, eqtt_to_assert, iff_weakening_uiff, implies_functionality_wrt_iff, iff_wf, rev_implies_wf, es-causl_weakening, es-le_weakening, es-locl_transitivity2, Id_wf, es-prior-interface-val-unique, es-causl-swellfnd, nat_wf, nat_properties, ge_wf, le_wf, es-causl_wf, assert_wf, true_wf, in-eclass_wf, ifthenelse_wf, false_wf, not_wf, assert_witness, es-E-interface_wf, es-locl_wf, es-threshold_wf, event-ordering+_inc, subtype_rel_self, es-base-E_wf, es-E_wf, bool_wf, event-ordering+_wf, eclass_wf, member_wf, subtype_rel_wf, es-interface-top, es-prior-interval-vals_wf, list_accum_wf, eclass-val_wf, assert_elim, es-interface-subtype_rel2, top_wf, es-prior-interface_wf1, subtype_base_sq, bool_subtype_base, es-prior-interface-vals_wf, uall_wf, uiff_inversion, sq_stable__assert, es-prior-interface_wf, intensional-universe_wf, is-prior-interface, is-threshold, not_assert_elim

\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[A:Type]. \mforall{}[X:EClass(A)]. \mforall{}[S:Type]. \mforall{}[init:S]. \mforall{}[f:S {}\mrightarrow{} A {}\mrightarrow{} S]. \mforall{}[test:S {}\mrightarrow{} A {}\mrightarrow{} \mBbbB{}]. \mforall{}[nxt:S \mtimes{} A {}\mrightarrow{} S]. \mforall{}[e:E]. ((\mforall{}[e':E(Threshold(init;f;test;nxt;X))] ((\muparrow{}e \mmember{}\msubb{} prior(Threshold(init;f;test;nxt;X))) \mwedge{} (prior(Threshold(init;f;test;nxt;X))(e) = e')) \mwedge{} (\muparrow{}e \mmember{}\msubb{} Threshold(init;f;test;nxt;X)) supposing ((\muparrow{}(test list\_accum(s,v.f s v;nxt Threshold(init;f;test;nxt;X)(e');X(e', e)) X(e))) and (\muparrow{}e \mmember{}\msubb{} X)) supposing (e' <loc e) \mwedge{} (\mforall{}e'':E(X) ((e' <loc e'') {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mneg{}\muparrow{}(test list\_accum(s,v.f s v;nxt Threshold(init;f;test;nxt;X)(e');X(e', e'')) X(e'')))))) \mwedge{} (\mneg{}\muparrow{}e \mmember{}\msubb{} prior(Threshold(init;f;test;nxt;X))) \mwedge{} (\muparrow{}e \mmember{}\msubb{} Threshold(init;f;test;nxt;X)) supposing ((\muparrow{}(test list\_accum(s,v.f s v;init;X(<e)) X(e))) and (\muparrow{}e \mmember{}\msubb{} X)) supposing \mforall{}e':E(X). ((e' <loc e) {}\mRightarrow{} (\mneg{}\muparrow{}(test list\_accum(s,v.f s v;init;X(<e')) X(e'))))) Date html generated: 2011_08_16-PM-05_12_41 Last ObjectModification: 2011_06_20-AM-01_13_59 Home Index