---

{ [size:]. [A:Type]. [num:A  ]. [P:A  ].
    (collectfilteracc2(size;x.num[x];v.P[v])
    = collect_accum(x.num[x];<0
      , tt
      >;p,v.let n,ok = p 
            in <n + 1, ok  P[v]>;p.(fst(p) = size) ((snd(p))))) }

{ Proof }

---

Definitions occuring in Statement :  collectfilteracc2: collectfilteracc2(size;v1.num[v1];v2.P[v2]),  collect_accum: collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]),  isl: isl(x),  eq_int: (i = j),  bor: p q,  band: p  q,  bnot: b,  assert: b,  btrue: tt,  bool: ,  nat_plus: ,  nat: ,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s],  pi1: fst(t),  pi2: snd(t),  le: A  B,  implies: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  function: x:A  B[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  union: left + right,  add: n + m,  natural_number: $n,  int: ,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  top: Top,  and: P  Q,  assert: b,  pi2: snd(t),  pi1: fst(t),  implies: P  Q,  isl: isl(x),  collectfilteracc2: collectfilteracc2(size;v1.num[v1];v2.P[v2]),  so_apply: x[s],  collect_accum: collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]),  btrue: tt,  band: p  q,  bor: p q,  bnot: b,  member: t  T,  spreadn: spread3,  ifthenelse: if b then t else f fi ,  bfalse: ff,  prop: ,  so_lambda: x.t[x],  all: x:A. B[x],  subtype: S  T,  has-value: has-value(a),  true: True,  nat_plus: ,  nat: ,  bool: ,  cand: A c B,  unit: Unit,  iff: P  Q,  false: False,  uimplies: b supposing a,  it: ,  not: A
Lemmas :  nat_wf,  bool_wf,  top_wf,  assert_wf,  pi2_wf,  pi1_wf_top,  isl_wf,  le_wf,  nat_plus_wf,  rational-has-value,  int-rational,  nat_properties,  int_inc,  lt_int_wf,  iff_weakening_uiff,  uiff_transitivity,  eqtt_to_assert,  assert_of_lt_int,  false_wf,  le_int_wf,  bnot_wf,  eqff_to_assert,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int,  eq_int_wf,  assert_of_eq_int,  btrue_wf,  true_wf,  not_wf,  assert_of_bnot,  not_functionality_wrt_uiff,  btrue_neq_bfalse,  bfalse_wf,  not_assert_elim,  assert_elim

---

\mforall{}[size:\mBbbN{}\msupplus{}].  \mforall{}[A:Type].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].
    (collectfilteracc2(size;x.num[x];v.P[v])
    =  collect\_accum(x.num[x];ɘ,  tt>p,v.let  n,ok  =  p 
                                                                              in  <n  +  1,  ok  \mwedge{}\msubb{}  P[v]>p.(fst(p)  =\msubz{}  size)  \mvee{}\msubb{}(\mneg{}\msubb{}(snd(p)))))


Date html generated: 2011_08_16-PM-05_29_19
Last ObjectModification: 2011_06_20-AM-01_24_48

Home Index