Nuprl Lemma : accum-class-programmable

{

[Info,A,B:Type].

[X:EClass(A)].

[base:A

B].

[f:B

A

B].
(accum-class(b,a.f[b;a];a.base[a];X)
=

B,r.
if (bag-size(B 0) =

1)
then if (bag-size(r) =

1)
            then {f[only(r);only(B 0)]}
            else {base[only(B 0)]}
            fi
       else {}
       fi |

i.X,(self)'|) }

{ Proof }

Definitions occuring in Statement : rec-combined-class: f|X,(self)'|, accum-class: accum-class(a,x.f[a; x];x.base[x];X), eclass: EClass(A[eo; e]), eq_int: (i =

j), ifthenelse: if b then t else f fi , uall:

[x:A]. B[x], so_apply: x[s1;s2], so_apply: x[s], apply: f a, lambda:

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

B[x], natural_number: $n, universe: Type, equal: s = t, bag-only: only(bs), bag-size: bag-size(bs), single-bag: {x}, empty-bag: {}
Definitions : permutation: permutation(T;L1;L2), IdLnk: IdLnk, Id: Id, append: as @ bs, locl: locl(a), Knd: Knd, list: type List, lt_int: i <z j, le_int: i

z j, limited-type: LimitedType, bfalse: ff, btrue: tt, 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_id: a = b, eq_lnk: a = b, es-eq-E: e = e', es-bless: e <loc e', es-ble: e

loc e', bimplies: p

q, band: p

q, bor: p

q, bnot:

b, unit: Unit, sq_stable: SqStable(P), union: left + right, or: P

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

l), quotient: x,y:A//B[x; y], lelt: i

j < k, grp_car: |g|, int_seg: {i..j

}, p-outcome: Outcome, prop:

, void: Void, false: False, set: {x:A| B[x]} , real:

, rationals:

, nat:

, int:

, implies: P

Q, eq_atom: eq_atom$n(x;y), atom: Atom, es-base-E: es-base-E(es), token: "$token", eq_atom: x =a y, record-select: r.x, dep-isect: Error :dep-isect, record+: record+, bool:

, assert:

b, subtype: S

T, event_ordering: EO, es-E: E, event-ordering+: EO+(Info), top: Top, bag: bag(T), pair: <a, b>, fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), le: A

B, ge: i

j , not:

A, less_than: a < b, uimplies: b supposing a, product: x:A

B[x], and: P

Q, uiff: uiff(P;Q), subtype_rel: A

r B, all:

x:A. B[x], axiom: Ax, empty-bag: {}, bag-only: only(bs), single-bag: {x}, bag-size: bag-size(bs), eq_int: (i =

j), ifthenelse: if b then t else f fi , lambda:

x.A[x], rec-combined-class: f|X,(self)'|, so_apply: x[s], apply: f a, so_apply: x[s1;s2], accum-class: accum-class(a,x.f[a; x];x.base[x];X), equal: s = t, universe: Type, so_lambda:

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

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

B[x], isect:

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

T, MaAuto: Error :MaAuto, CollapseTHEN: Error :CollapseTHEN, Auto: Error :Auto, so_lambda:

x.t[x], natural_number: $n, CollapseTHENA: Error :CollapseTHENA, Try: Error :Try, Complete: Error :Complete, eclass: EClass(A[eo; e]), tactic: Error :tactic, primed-class: Prior(X), D: Error :D, cond-class: [X?Y], eq_knd: a = b, fpf-dom: x

dom(f), eq_bool: p =b q, es-E-interface: E(X), eclass-val: X(e), in-eclass: e

X, sq_type: SQType(T), true: True, squash:

T, ite: ite(b;x;y), decide: case b of inl(x) => s[x] | inr(y) => t[y], HypSubst: Error :HypSubst, sv-class: Singlevalued(X), bag_size_single: bag_size_single{bag_size_single_compseq_tag_def:o}(x), bag_size_empty: bag_size_empty{bag_size_empty_compseq_tag_def:o}, rev_implies: P

Q, iff: P

Q, RepeatFor: Error :RepeatFor, Repeat: Error :Repeat, sqequal: s ~ t, ParallelOp: Error :ParallelOp, es-causl: (e < e'), minus: -n, add: n + m, subtract: n - m, exists:

x:A. B[x], strongwellfounded: SWellFounded(R[x; y]), es-interface-predecessors:

(X)(e), accum_list: accum_list(a,x.f[a; x];x.base[x];L), length: ||as||, es-loc: loc(e), Subst': Error :Subst', bag_only_single: bag_only_single{bag_only_single_compseq_tag_def:o}(x), proper-iseg: L1 < L2, iseg: l1

l2, l_exists: (

x

L. P[x]), multiply: n * m, gt: i > j, map: map(f;as), nil: [], cons: [car / cdr], tl: tl(l), hd: hd(l), es-prior-val: (X)', es-prior-interface: prior(X), accum_list_cons: accum_list_cons_compseq_tag_def, RepUR: Error :RepUR, es-le: e

loc e' , es-locl: (e <loc e'), es-p-le: e p

e', es-causle: e c

e', es-p-locl: e p< e', causal-predecessor: causal-predecessor(es;p), record: record(x.T[x]), fpf-cap: f(x)?z, label: ...$L... t, atom: Atom$n, filter: filter(P;l), intensional-universe: IType, list_accum: list_accum(x,a.f[x; a];y;l), cand: A c

B, 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
Lemmas : sq_stable__assert, es-prior-val_wf, btrue_wf, not_assert_elim, primed-class-prior-val, es-is-prior-interface, es-locl_wf, length-append, list-set-type2, list_accum_wf, list_accum_append, set_subtype_base, list_subtype_base, es-prior-interface-same, intensional-universe_wf, list-subtype, l_member_wf, length_nil, non_neg_length, length_cons, length_append, es-prior-interface-causl, eclass-val_wf2, assert_elim, bool_subtype_base, es-prior-interface_wf1, append_wf, es-prior-interface_wf, es-interface-subtype_rel2, es-interface-predecessors-nonempty, es-interface-predecessors-step, length_wf1, es-interface-val_wf2, length_wf_nat, pos-length, equal-nil-sq-nil, es-loc_wf, pos_length2, es-causl-swellfnd, accum_list_wf, es-E-interface_wf, Id_wf, es-interface-predecessors_wf, accum-class-val, nat_properties, ge_wf, es-causl_wf, is-accum-class, es-interface-extensionality, rev_implies_wf, iff_wf, sv-class_wf, es-interface-top, subtype_rel_wf, eclass-val_wf, primed-class_wf, top_wf, in-eclass_wf, subtype_base_sq, true_wf, squash_wf, ite_wf, bag_wf, ifthenelse_wf, single-bag_wf, accum-class_wf, eclass_wf, event-ordering+_wf, es-E_wf, event-ordering+_inc, uall_wf, es-base-E_wf, subtype_rel_self, member_wf, rec-combined-class_wf, le_wf, not_wf, false_wf, nat_wf, int_seg_wf, eq_int_wf, bag-size_wf, bag-only_wf, bool_wf, uiff_transitivity, eqtt_to_assert, assert_of_eq_int, assert_wf, eqff_to_assert, assert_of_bnot, not_functionality_wrt_uiff, bnot_wf, permutation_wf, empty-bag_wf

\mforall{}[Info,A,B:Type]. \mforall{}[X:EClass(A)]. \mforall{}[base:A {}\mrightarrow{} B]. \mforall{}[f:B {}\mrightarrow{} A {}\mrightarrow{} B]. (accum-class(b,a.f[b;a];a.base[a];X) = \mlambda{}B,r. if (bag-size(B 0) =\msubz{} 1) then if (bag-size(r) =\msubz{} 1) then \{f[only(r);only(B 0)]\} else \{base[only(B 0)]\} fi else \{\} fi |\mlambda{}i.X,(self)'|) Date html generated: 2011_08_16-PM-06_07_54 Last ObjectModification: 2011_01_22-PM-08_09_17 Home Index