---

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

{ Proof }

---

Definitions occuring in Statement :  collect_accm: collect_accm(v.P[v];v.num[v]),  length: ||as||,  assert: b,  bool: ,  nat: ,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s],  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,  so_apply: x[s],  and: P  Q,  top: Top,  collect_accm: collect_accm(v.P[v];v.num[v]),  spreadn: spread3,  ifthenelse: if b then t else f fi ,  ge: i  j ,  label: ...$L... t,  ycomb: Y,  le: A  B,  false: False,  all: x:A. B[x],  btrue: tt,  prop: ,  cand: A c B,  bfalse: ff,  subtype: S  T,  bool: ,  nat: ,  unit: Unit,  iff: P  Q,  uimplies: b supposing a,  it: ,  has-value: has-value(a)
Lemmas :  length_wf1,  length_nil,  length_wf_nat,  top_wf,  length_cons,  non_neg_length,  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  rational-has-value,  int-rational,  nat_wf,  lt_int_wf,  uiff_transitivity,  assert_of_lt_int,  le_wf,  le_int_wf,  bnot_wf,  eqff_to_assert,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int,  length_wf2,  not_wf,  append_wf,  length_append,  assert_of_bnot

---

\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{}  \mBbbZ{}
                                                                      \mtimes{}  \{L:A  List|  (0  <  ||L||)  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\} 
                                                                      \mtimes{}  (\{L:A  List|  (0  <  ||L||)  \mwedge{}  (\muparrow{}P[L])\}    +  Top)
                                                                      {}\mrightarrow{}  A
                                                                      {}\mrightarrow{}  (\mBbbZ{}
                                                                            \mtimes{}  \{L:A  List|  (0  <  ||L||)  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\} 
                                                                            \mtimes{}  (\{L:A  List|  (0  <  ||L||)  \mwedge{}  (\muparrow{}P[L])\}    +  Top)))


Date html generated: 2011_08_16-AM-11_04_29
Last ObjectModification: 2011_06_18-AM-09_37_14

Home Index