{ [Info,A,B:Type]. [X:EClass(A)]. [x:B]. [f:B  A  B].
    (es-interface-accum(f;x;X)
    = B,r.
       if (bag-size(B 0) = 1)
       then if (bag-size(r) = 1)
            then {f[only(r);only(B 0)]}
            else {f[x;only(B 0)]}
            fi 
       else {}
       fi |i.X,(self)'|) }

{ Proof }


Definitions occuring in Statement :  rec-combined-class: f|X,(self)'|,  es-interface-accum: es-interface-accum(f;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],  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: (xL.P[x])_b,  bl-exists: (xL.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),  so_apply: x[s],  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,  top: Top,  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,  axiom: Ax,  lambda: x.A[x],  rec-combined-class: f|X,(self)'|,  es-interface-accum: es-interface-accum(f;x;X),  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,  empty-bag: {},  apply: f a,  bag-only: only(bs),  so_apply: x[s1;s2],  single-bag: {x},  primed-class: Prior(X),  natural_number: $n,  bag-size: bag-size(bs),  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  bag: bag(T),  equal: s = t,  es-E: E,  all: x:A. B[x],  event-ordering+: EO+(Info),  CollapseTHEN: Error :CollapseTHEN,  MaAuto: Error :MaAuto,  Auto: Error :Auto,  so_lambda: x.t[x],  CollapseTHENA: Error :CollapseTHENA,  Try: Error :Try,  Complete: Error :Complete,  eclass: EClass(A[eo; e]),  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],  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,  D: Error :D,  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),  list_accum: list_accum(x,a.f[x; a];y;l),  tag-by: zT,  record: record(x.T[x]),  fset: FSet{T},  dataflow: dataflow(A;B),  isect2: T1  T2,  b-union: A  B,  fpf-sub: f  g,  deq: EqDecider(T),  ma-state: State(ds),  class-program: ClassProgram(T),  fpf-cap: f(x)?z,  intensional-universe: IType,  suptype: suptype(S; T),  es-loc: loc(e),  Subst': Error :Subst',  bag_only_single: bag_only_single{bag_only_single_compseq_tag_def:o}(x),  nil: [],  cons: [car / cdr],  tl: tl(l),  hd: hd(l),  tactic: Error :tactic,  es-prior-val: (X)',  es-prior-interface: prior(X),  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),  atom: Atom$n,  filter: filter(P;l),  length: ||as||,  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)
Lemmas :  sq_stable__assert,  es-prior-val_wf,  btrue_wf,  not_assert_elim,  primed-class-prior-val,  es-is-prior-interface,  es-locl_wf,  list_accum_append,  length_wf_nat,  set_subtype_base,  list_subtype_base,  length_wf1,  es-interface-predecessors-nonempty,  es-prior-interface-same,  list-subtype,  l_member_wf,  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-step,  es-interface-val_wf2,  es-loc_wf,  intensional-universe_wf,  es-interface-subtype_rel,  es-interface-accum-val,  es-interface-predecessors_wf,  Id_wf,  es-E-interface_wf,  list_accum_wf,  es-causl-swellfnd,  nat_properties,  ge_wf,  es-causl_wf,  is-interface-accum,  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,  es-interface-accum_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{}[x:B].  \mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].
    (es-interface-accum(f;x;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  \{f[x;only(B  0)]\}  fi 
          else  \{\}
          fi  |\mlambda{}i.X,(self)'|)


Date html generated: 2011_08_16-PM-06_07_28
Last ObjectModification: 2011_06_20-AM-01_48_18

Home Index