---

{ [A,B:Type]. [P:B  ]. [num:A  ]. [init:B]. [f:B  A  B].
    (collect_accum(x.num[x];init;a,v.f[a;v];a.P[a])  {s:  B  (B + Top)| 
                                                       (isl(snd(snd(s))))
                                                        (1  (fst(s)))} 
                                                       A
                                                       {s:  B  (B + Top)| 
                                                          (isl(snd(snd(s))))
                                                           (1  (fst(s)))} ) }

{ Proof }

---

Definitions occuring in Statement :  collect_accum: collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]),  isl: isl(x),  assert: b,  bool: ,  nat: ,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s1;s2],  so_apply: x[s],  pi1: fst(t),  pi2: snd(t),  le: A  B,  implies: P  Q,  member: t  T,  set: {x:A| B[x]} ,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  natural_number: $n,  int: ,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  top: Top,  implies: P  Q,  assert: b,  isl: isl(x),  pi2: snd(t),  pi1: fst(t),  collect_accum: collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]),  so_apply: x[s],  so_apply: x[s1;s2],  spreadn: spread3,  ifthenelse: if b then t else f fi ,  all: x:A. B[x],  prop: ,  so_lambda: x.t[x],  subtype: S  T,  btrue: tt,  bfalse: ff,  bool: ,  nat: ,  unit: Unit,  iff: P  Q,  and: P  Q,  uimplies: b supposing a,  false: False,  it: ,  has-value: has-value(a)
Lemmas :  assert_wf,  isl_wf,  top_wf,  pi2_wf,  le_wf,  pi1_wf_top,  bool_wf,  iff_weakening_uiff,  eqtt_to_assert,  rational-has-value,  int-rational,  nat_wf,  ifthenelse_wf,  lt_int_wf,  uiff_transitivity,  assert_of_lt_int,  bfalse_wf,  le_int_wf,  bnot_wf,  eqff_to_assert,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int,  btrue_wf,  not_wf,  assert_of_bnot,  false_wf

---

\mforall{}[A,B:Type].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[init:B].  \mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].
    (collect\_accum(x.num[x];init;a,v.f[a;v];a.P[a])  \mmember{}  \{s:\mBbbZ{}  \mtimes{}  B  \mtimes{}  (B  +  Top)| 
                                                                                                          (\muparrow{}isl(snd(snd(s))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\} 
                                                                                                        {}\mrightarrow{}  A
                                                                                                        {}\mrightarrow{}  \{s:\mBbbZ{}  \mtimes{}  B  \mtimes{}  (B  +  Top)| 
                                                                                                                (\muparrow{}isl(snd(snd(s))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\}  )


Date html generated: 2011_08_16-AM-11_04_52
Last ObjectModification: 2011_06_18-AM-09_37_32

Home Index