Nuprl Lemma : es-collect-filter-max

{

[Info,A1,A2,T:Type].

[R:

T

].

[g1:A1

T].

[g2:A2

T].

[f1:A1

].

[f2:A2

].

[X1:EClass(A1)].

[X2:EClass(A2)].

[size:

].

[num1:A1

].

[num2:A2

].

[P1:A1

].

[P2:A2

].
    ((let n,mx,v = tr in
       <n
       , mx
       , g1[v]> where tr from ...)
       = (let n,mx,v = tr in
         <n
         , mx
         , g2[v]> where tr from ...)) supposing
       ((

es:EO+(Info).

e:E.
((

e

X1

e

X2)

((

e

X1)

(

e

X2)

((

P1[X1(e)]

P2[X2(e)])

(num1[X1(e)] = num2[X2(e)])

(f1[X1(e)] = f2[X2(e)])

(g1[X1(e)] = g2[X2(e)]))))) and
(

a:A2. R[f2[a];g2[a]]) and
(

a:A1. R[f1[a];g1[a]])) }

{ Proof }

Definitions occuring in Statement : es-collect-filter-max: es-collect-filter-max, map-class: (f[v] where v from X), eclass-val: X(e), in-eclass: e

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

b, bool:

, nat_plus:

, nat:

, spreadn: spread3, uimplies: b supposing a, uall:

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

, so_apply: x[s1;s2], so_apply: x[s], all:

x:A. B[x], iff: P

Q, implies: P

Q, and: P

Q, set: {x:A| B[x]} , function: x:A

B[x], pair: <a, b>, product: x:A

B[x], int:

, universe: Type, equal: s = t
Definitions : fpf-dom: x

dom(f), so_lambda:

x.t[x], fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), le: A

B, ge: i

j , not:

A, uiff: uiff(P;Q), axiom: Ax, es-collect-filter-max: es-collect-filter-max, pair: <a, b>, spreadn: spread3, map-class: (f[v] where v from X), real:

, grp_car: |g|, es-E-interface: E(X), eclass-val: X(e), decide: case b of inl(x) => s[x] | inr(y) => t[y], less_than: a < b, rev_implies: P

Q, in-eclass: e

X, cand: A c

B, assert:

b, iff: P

Q, implies: P

Q, product: x:A

B[x], and: P

Q, so_apply: x[s], so_apply: x[s1;s2], uimplies: b supposing a, bool:

, set: {x:A| B[x]} , nat:

, nat_plus:

, union: left + right, subtype: S

T, subtype_rel: A

r B, eq_atom: eq_atom$n(x;y), atom: Atom, apply: f a, top: Top, es-base-E: es-base-E(es), token: "$token", eq_atom: x =a y, ifthenelse: if b then t else f fi , record-select: r.x, dep-isect: Error :dep-isect, record+: record+, event_ordering: EO, es-E: E, event-ordering+: EO+(Info), lambda:

x.A[x], isect:

x:A. B[x], all:

x:A. B[x], so_lambda:

x y.t[x; y], eclass: EClass(A[eo; e]), int:

, prop:

, function: x:A

B[x], uall:

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

T, equal: s = t, universe: Type, tactic: Error :tactic, sqequal: s ~ t, 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, fpf-cap: f(x)?z, record: record(x.T[x]), 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, es-collect-filter-max-aux: es-collect-filter-max-aux(X;size;v.num[v];v.P[v];v.f[v]), es-collect-accum: es-collect-accum(X;x.num[x];init;a,v.f[a; v];a.P[a]), es-interface-accum: es-interface-accum(f;x;X), collect_filter: collect_filter(), collect_accum: collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]), exists:

x:A. B[x], cond-class: [X?Y], void: Void, true: True, sq_type: SQType(T), false: False, spread: spread def, Knd: Knd, IdLnk: IdLnk, Id: Id, eq_knd: a = b, list: type List, sq_stable: SqStable(P), or: P

Q, guard: {T}, l_member: (x

l), limited-type: LimitedType, proper-iseg: L1 < L2, iseg: l1

l2, l_exists: (

x

L. P[x]), multiply: n * m, gt: i > j, map: map(f;as), es-locl: (e <loc e'), bfalse: ff, unit: Unit, int_eq: if a=b then c else d, btrue: tt, atom_eq: atomeqn def, append: as @ bs, locl: locl(a), atom: Atom$n, isl: isl(x), can-apply: can-apply(f;x), int_nzero:

, mapfilter: mapfilter(f;P;L), natural_number: $n, alle-lt:

e<e'.P[e], es-interface-predecessors:

(X)(e), eq_int: (i =

j), band: p

q, filter: filter(P;l), length: ||as||, es-loc: loc(e), es-first-at: e is first@ i s.t. e.P[e], infix_ap: x f y, es-causl: (e < e'), MaAuto: Error :MaAuto, Auto: Error :Auto, CollapseTHEN: Error :CollapseTHEN, RepeatFor: Error :RepeatFor, CollapseTHENA: Error :CollapseTHENA, Complete: Error :Complete, Try: Error :Try, Repeat: Error :Repeat, list-max: list-max(x.f[x];L), combination: Combination(n;T), listp: A List

, nil: [], Unfold: Error :Unfold, ExRepD: Error :ExRepD, it:

, pi2: snd(t), pi1: fst(t), AllHyps: Error :AllHyps, rationals:

, add: n + m
Lemmas : non_neg_length, nat_properties, pi1_wf_top, pi2_wf, product_subtype_base, list-max-map, list_subtype_base, map_wf, list-max_wf, set_subtype_base, es-interface-predecessors-equal, collect-filter-max-val, map-class-val, length-map, squash_wf, int_subtype_base, es-interface-predecessors-equal-subtype, iff_imp_equal_bool, es-loc_wf, Id_wf, es-E-interface_wf, filter_wf, length_wf1, es-interface-predecessors_wf, es-first-at_wf, is-collect-filter-max, iff_weakening_uiff, alle-lt_wf, le_wf, band_wf, eq_int_wf, length_wf_nat, list-subtype, l_member_wf, filter_type, assert-eq-id, subtype_base_sq, bool_subtype_base, assert_elim, nat_plus_properties, mapfilter_wf, btrue_wf, bfalse_wf, unit_wf, es-interface-val_wf2, not_wf, es-locl_wf, pos_length2, pos-length, equal-nil-sq-nil, subtype_rel_wf, uiff_inversion, es-interface-extensionality, map-class_wf, false_wf, ifthenelse_wf, true_wf, top_wf, rev_implies_wf, sq_stable__assert, intensional-universe_wf, is-map-class, es-interface-subtype_rel2, member_wf, eclass_wf, in-eclass_wf, assert_wf, es-interface-top, iff_wf, event-ordering+_inc, subtype_rel_self, es-base-E_wf, es-E_wf, event-ordering+_wf, bool_wf, nat_wf, nat_plus_wf, eclass-val_wf, es-collect-filter-max_wf

\mforall{}[Info,A1,A2,T:Type]. \mforall{}[R:\mBbbZ{} {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]. \mforall{}[g1:A1 {}\mrightarrow{} T]. \mforall{}[g2:A2 {}\mrightarrow{} T]. \mforall{}[f1:A1 {}\mrightarrow{} \mBbbZ{}]. \mforall{}[f2:A2 {}\mrightarrow{} \mBbbZ{}]. \mforall{}[X1:EClass(A1)]. \mforall{}[X2:EClass(A2)]. \mforall{}[size:\mBbbN{}\msupplus{}]. \mforall{}[num1:A1 {}\mrightarrow{} \mBbbN{}]. \mforall{}[num2:A2 {}\mrightarrow{} \mBbbN{}]. \mforall{}[P1:A1 {}\mrightarrow{} \mBbbB{}]. \mforall{}[P2:A2 {}\mrightarrow{} \mBbbB{}]. ((let n,mx,v = tr in <n, mx, g1[v]> where tr from Collect(size v's from X1 with maximum num1[v] such that P1[v] return <num1[v],n,v> with n = maximum f1[v])) = (let n,mx,v = tr in <n , mx , g2[v]> where tr from Collect(size v's from X2 with maximum num2[v] such that P2[v] return <num2[v],n,v> with n = maximum f2[v]))) supposing ((\mforall{}es:EO+(Info). \mforall{}e:E. ((\muparrow{}e \mmember{}\msubb{} X1 \mLeftarrow{}{}\mRightarrow{} \muparrow{}e \mmember{}\msubb{} X2) \mwedge{} ((\muparrow{}e \mmember{}\msubb{} X1) {}\mRightarrow{} (\muparrow{}e \mmember{}\msubb{} X2) {}\mRightarrow{} ((\muparrow{}P1[X1(e)] \mLeftarrow{}{}\mRightarrow{} \muparrow{}P2[X2(e)]) \mwedge{} (num1[X1(e)] = num2[X2(e)]) \mwedge{} (f1[X1(e)] = f2[X2(e)]) \mwedge{} (g1[X1(e)] = g2[X2(e)]))))) and (\mforall{}a:A2. R[f2[a];g2[a]]) and (\mforall{}a:A1. R[f1[a];g1[a]])) Date html generated: 2011_08_16-PM-05_33_46 Last ObjectModification: 2010_11_29-PM-06_25_24 Home Index