Nuprl Lemma : collect-filter-max-val

[Info:Type].

[es:EO+(Info)].

[A:Type].

[f:A

].

[X:EClass(A)].

[size:

].

[num:A

].

[P:A

].

[e:E].
Collect(size v's from X with maximum num[v] such that P[v] return <num[v],n,v> with n = maximum f[v])(e)
= <num[X(e)], list-max(v.f[v];mapfilter(

e.X(e);

e'.(num[X(e')] =

num[X(e)]);

(X)(e)))>
supposing

e

Collect(size v's from X with maximum num[v] such that P[v]
return <num[v],n,v> with n = maximum f[v])

Proof not projected

Definitions occuring in Statement : es-collect-filter-max: Collect(size v's from X with maximum num[v] such that P[v] return <num[v],n,v> with n = maximum f[v]), es-interface-predecessors:

(X)(e), eclass-val: X(e), in-eclass: e

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

j), assert:

b, bool:

, nat_plus:

, nat:

, uimplies: b supposing a, uall:

[x:A]. B[x], so_apply: x[s], set: {x:A| B[x]} , lambda:

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

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

B[x], int:

, universe: Type, equal: s = t, mapfilter: mapfilter(f;P;L), list-max: list-max(x.f[x];L)
Definitions : so_lambda:

x y.t[x; y], all:

x:A. B[x], top: Top, so_lambda:

x.t[x], member: t

T, so_apply: x[s], es-collect-filter-max: Collect(size v's from X with maximum num[v] such that P[v] return <num[v],n,v> with n = maximum f[v]), and: P

Q, ifthenelse: if b then t else f fi , btrue: tt, true: True, squash:

T, subtype: S

T, pi2: snd(t), pi1: fst(t), assert:

b, prop:

, so_apply: x[s1;s2], cand: A c

B, uall:

[x:A]. B[x], uiff: uiff(P;Q), uimplies: b supposing a, guard: {T}, sq_type: SQType(T), sq_stable: SqStable(P), es-E-interface: E(X), implies: P

Q, nat:

, list-max: list-max(x.f[x];L)
Lemmas : eclass_wf, nat_plus_wf, bool_wf, es-collect-filter-max_wf, in-eclass_wf, event-ordering+_wf, event-ordering+_inc, es-E_wf, isl_wf, assert_wf, top_wf, nat_wf, es-interface-subtype_rel2, es-collect-filter-max-aux_wf, map-class-val, is-collect-filter-max, collect-filter-max-aux-val, and_wf, bool_subtype_base, subtype_base_sq, assert_elim, outl_wf, pi1_wf_top, equal_wf, es-interface-val_wf2, sq_stable__assert, eq_int_wf, es-interface-predecessors_wf, es-loc_wf, Id_wf, es-interface-top, es-E-interface_wf, mapfilter_wf, list-max_wf, eclass-val_wf, pi2_wf, list-max-aux-property

\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[A:Type]. \mforall{}[f:A {}\mrightarrow{} \mBbbZ{}]. \mforall{}[X:EClass(A)]. \mforall{}[size:\mBbbN{}\msupplus{}]. \mforall{}[num:A {}\mrightarrow{} \mBbbN{}]. \mforall{}[P:A {}\mrightarrow{} \mBbbB{}]. \mforall{}[e:E]. Collect(size v's from X with maximum num[v] such that P[v] return <num[v],n,v> with n = maximum f[v])(e) = <num[X(e)], list-max(v.f[v];mapfilter(\mlambda{}e.X(e);\mlambda{}e'.(num[X(e')] =\msubz{} num[X(e)]);\mleq{}(X)(e)))> supposing \muparrow{}e \mmember{}\msubb{} Collect(size v's from X with maximum num[v] such that P[v] return <num[v],n,v> with n = maximum f[v]) Date html generated: 2012_01_23-PM-12_28_02 Last ObjectModification: 2011_12_13-PM-03_03_13 Home Index