---

{ [A:Type]. [P:{L:A List| 0 < ||L||}   ]. [num:A  ].
    (collect_accm(v.P[v];v.num[v])
     {s:
        {L:A List| (0 < ||L||)  (P[L])} 
        ({L:A List| (0 < ||L||)  (P[L])}  + Top)| 
       (isl(snd(snd(s))))  (1  (fst(s)))} 
       A
       {s:
           {L:A List| (0 < ||L||)  (P[L])} 
           ({L:A List| (0 < ||L||)  (P[L])}  + Top)| 
          (isl(snd(snd(s))))  (1  (fst(s)))} ) }

{ Proof }

---

Definitions occuring in Statement :  collect_accm: collect_accm(v.P[v];v.num[v]),  length: ||as||,  isl: isl(x),  assert: b,  bool: ,  nat: ,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s],  pi1: fst(t),  pi2: snd(t),  le: A  B,  not: A,  implies: P  Q,  and: P  Q,  member: t  T,  less_than: a < b,  set: {x:A| B[x]} ,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  list: type List,  natural_number: $n,  int: ,  universe: Type
Definitions :  uall: [x:A]. B[x],  length: ||as||,  member: t  T,  implies: P  Q,  not: A,  assert: b,  so_apply: x[s],  and: P  Q,  top: Top,  isl: isl(x),  pi2: snd(t),  le: A  B,  pi1: fst(t),  collect_accm: collect_accm(v.P[v];v.num[v]),  spreadn: spread3,  ifthenelse: if b then t else f fi ,  all: x:A. B[x],  prop: ,  cand: A c B,  so_lambda: x.t[x],  ge: i  j ,  label: ...$L... t,  ycomb: Y,  false: False,  btrue: tt,  bfalse: ff,  subtype: S  T,  bool: ,  nat: ,  unit: Unit,  iff: P  Q,  uimplies: b supposing a,  it: ,  has-value: has-value(a)
Lemmas :  assert_wf,  isl_wf,  length_wf1,  top_wf,  pi2_wf,  not_wf,  le_wf,  pi1_wf_top,  length_nil,  length_wf_nat,  length_cons,  non_neg_length,  bool_wf,  iff_weakening_uiff,  eqtt_to_assert,  rational-has-value,  int-rational,  nat_wf,  lt_int_wf,  uiff_transitivity,  assert_of_lt_int,  le_int_wf,  bnot_wf,  eqff_to_assert,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int,  length_wf2,  append_wf,  length_append,  assert_of_bnot,  false_wf

---

\mforall{}[A:Type].  \mforall{}[P:\{L:A  List|  0  <  ||L||\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].
    (collect\_accm(v.P[v];v.num[v])  \mmember{}  \{s:\mBbbZ{}
                                                                        \mtimes{}  \{L:A  List|  (0  <  ||L||)  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\} 
                                                                        \mtimes{}  (\{L:A  List|  (0  <  ||L||)  \mwedge{}  (\muparrow{}P[L])\}    +  Top)| 
                                                                        (\muparrow{}isl(snd(snd(s))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\} 
                                                                      {}\mrightarrow{}  A
                                                                      {}\mrightarrow{}  \{s:\mBbbZ{}
                                                                              \mtimes{}  \{L:A  List|  (0  <  ||L||)  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\} 
                                                                              \mtimes{}  (\{L:A  List|  (0  <  ||L||)  \mwedge{}  (\muparrow{}P[L])\}    +  Top)| 
                                                                              (\muparrow{}isl(snd(snd(s))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\}  )


Date html generated: 2011_08_16-AM-11_04_37
Last ObjectModification: 2011_06_18-AM-09_37_20

Home Index