Nuprl Lemma : prior-imax-class-lb2

{

[Info:Type].

[es:EO+(Info)].

[e:E].

[n:

].

[A:Type].

[f:A

].

[Z:EClass(A)].
uiff(if e

((maximum f[x]

0 with x from Z))'
then ((maximum f[x]

0 with x from Z))'(e)
else -1
fi

n;

[e':E(Z)]. f[Z(e')]

n supposing e'

loc e )
supposing

e

Z }

{ Proof }

Definitions occuring in Statement : es-prior-val: (X)', imax-class: (maximum f[v]

lb with v from X), es-E-interface: E(X), eclass-val: X(e), in-eclass: e

X, eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-le: e

loc e' , es-E: E, assert:

b, ifthenelse: if b then t else f fi , nat:

, uiff: uiff(P;Q), uimplies: b supposing a, uall:

[x:A]. B[x], so_apply: x[s], le: A

B, not:

A, function: x:A

B[x], minus: -n, natural_number: $n, universe: Type
Definitions : cond-class: [X?Y], eq_knd: a = b, fpf-dom: x

dom(f), limited-type: LimitedType, bfalse: ff, eq_bool: p =b q, lt_int: i <z j, le_int: i

z j, eq_int: (i =

j), null: null(as), set_blt: a <

b, grp_blt: a <

b, infix_ap: x f y, dcdr-to-bool: [d]

, bl-all: (

x

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

x

L.P[x])_b, b-exists: (

i<n.P[i])_b, eq_type: eq_type(T;T'), qeq: qeq(r;s), q_less: q_less(r;s), q_le: q_le(r;s), deq-member: deq-member(eq;x;L), deq-disjoint: deq-disjoint(eq;as;bs), deq-all-disjoint: deq-all-disjoint(eq;ass;bs), eq_str: Error :eq_str, eq_id: a = b, eq_lnk: a = b, es-eq-E: e = e', bimplies: p

q, band: p

q, bor: p

q, bnot:

b, unit: Unit, isl: isl(x), can-apply: can-apply(f;x), imax: imax(a;b), length: ||as||, es-locl: (e <loc e'), l_member: (x

l), fpf: a:A fp-> B[a], guard: {T}, btrue: tt, sq_type: SQType(T), bool:

, true: True, real:

, grp_car: |g|, strong-subtype: strong-subtype(A;B), or: P

Q, ge: i

j , minus: -n, natural_number: $n, imax-class: (maximum f[v]

lb with v from X), es-prior-val: (X)', eclass-val: X(e), so_apply: x[s], rev_implies: P

Q, iff: P

Q, so_lambda:

x.t[x], less_than: a < b, es-le: e

loc e' , es-E-interface: E(X), pair: <a, b>, void: Void, product: x:A

B[x], and: P

Q, uiff: uiff(P;Q), decide: case b of inl(x) => s[x] | inr(y) => t[y], implies: P

Q, false: False, le: A

B, int:

, in-eclass: e

X, union: left + right, prop:

, not:

A, uimplies: b supposing a, lambda:

x.A[x], so_lambda:

x y.t[x; y], eclass: EClass(A[eo; e]), set: {x:A| B[x]} , assert:

b, nat:

, 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, dep-isect: Error :dep-isect, eq_atom: x =a y, eq_atom: eq_atom$n(x;y), record+: record+, universe: Type, all:

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

B[x], isect:

x:A. B[x], uall:

[x:A]. B[x], es-E: E, event_ordering: EO, equal: s = t, event-ordering+: EO+(Info), member: t

T, tactic: Error :tactic, exists:

x:A. B[x], es-causl: (e < e'), sqequal: s ~ t, es-loc: loc(e), es-causle: e c

e', es-init: es-init(es;e), es-pred: pred(e), Id: Id, existse-before:

e<e'.P[e], existse-le:

e

e'.P[e], alle-lt:

e<e'.P[e], alle-le:

e

e'.P[e], alle-between1:

e

[e1,e2).P[e], existse-between1:

e

[e1,e2).P[e], alle-between2:

e

[e1,e2].P[e], existse-between2:

e

[e1,e2].P[e], existse-between3:

e

(e1,e2].P[e], same-thread: same-thread(es;p;e;e'), es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), es-fset-loc: i

locs(s), decidable: Dec(P), squash:

T, record: record(x.T[x]), it:

, es-prior-interface: prior(X), es-interface-at: X@i, intensional-universe: IType, tag-by: z

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

T2, b-union: A

B, list: type List, fpf-cap: f(x)?z, 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, sq_stable: SqStable(P), cand: A c

B
Lemmas : is-prior-val, sq_stable__assert, intensional-universe_wf, set_subtype_base, squash_wf, es-loc_wf, decidable__es-locl, es-le-not-locl, es-le-loc, btrue_neq_bfalse, not_assert_elim, decidable__es-le, imax-class-lb, iff_functionality_wrt_iff, es-locl_wf, es-causle-le, es-causl_wf, Id_wf, es-locl_transitivity1, es-le_weakening, is-imax-class, prior-val-val, int_subtype_base, false_wf, not_wf, le_wf, ifthenelse_wf, uall_wf, es-E-interface_wf, es-le_wf, uiff_wf, es-interface-top, member_wf, eclass_wf, in-eclass_wf, assert_wf, event-ordering+_wf, event-ordering+_inc, subtype_rel_self, es-base-E_wf, es-E_wf, nat_wf, eclass-val_wf, true_wf, bool_wf, subtype_base_sq, bool_subtype_base, assert_elim, subtype_rel_wf, imax-class_wf, es-prior-val_wf, top_wf, rev_implies_wf, iff_wf, nat_properties, es-interface-subtype_rel2, iff_weakening_uiff, eqtt_to_assert, uiff_transitivity, eqff_to_assert, assert_of_bnot, bnot_wf

\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[n:\mBbbN{}]. \mforall{}[A:Type]. \mforall{}[f:A {}\mrightarrow{} \mBbbN{}]. \mforall{}[Z:EClass(A)]. uiff(if e \mmember{}\msubb{} ((maximum f[x] \mgeq{} 0 with x from Z))' then ((maximum f[x] \mgeq{} 0 with x from Z))'(e) else -1 fi \mleq{} n;\mforall{}[e':E(Z)]. f[Z(e')] \mleq{} n supposing e' \mleq{}loc e ) supposing \mneg{}\muparrow{}e \mmember{}\msubb{} Z Date html generated: 2011_08_16-PM-05_20_19 Last ObjectModification: 2011_06_20-AM-01_21_19 Home Index