---

{ [n,m:]. [L:{dv:ClassDerivation| WF(dv)}  List].
    (pack-cdv-args(n;m;L)  {dv:ClassDerivation| WF(dv)} ) supposing 
       ((||L|| = (n + m)) and 
       (0 < (n + m))) }

{ Proof }

---

Definitions occuring in Statement :  pack-cdv-args: pack-cdv-args(n;m;L),  cdv-wf: WF(dv),  classderiv: ClassDerivation,  length: ||as||,  nat: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T,  less_than: a < b,  set: {x:A| B[x]} ,  list: type List,  add: n + m,  natural_number: $n,  int: ,  equal: s = t
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  member: t  T,  pack-cdv-args: pack-cdv-args(n;m;L),  ifthenelse: if b then t else f fi ,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  prop: ,  bfalse: ff,  listp: A List,  cdv-wf: WF(dv),  not: A,  le: A  B,  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  int_iseg: {i...j},  false: False,  nat: ,  bool: ,  unit: Unit,  sq_type: SQType(T),  guard: {T},  it:
Lemmas :  eq_int_wf,  bool_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_eq_int,  list-to-cdv_wf,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff,  length_wf1,  classderiv_wf,  cdv-wf_wf,  nat_wf,  subtype_base_sq,  int_subtype_base,  lt_int_wf,  assert_of_lt_int,  cdvdelay_wf,  it_wf,  firstn_wf,  length_firstn,  le_wf,  nth_tl_wf,  length_nth_tl,  cdvpair_wf

---

\mforall{}[n,m:\mBbbN{}].  \mforall{}[L:\{dv:ClassDerivation|  WF(dv)\}    List].
    (pack-cdv-args(n;m;L)  \mmember{}  \{dv:ClassDerivation|  WF(dv)\}  )  supposing 
          ((||L||  =  (n  +  m))  and 
          (0  <  (n  +  m)))


Date html generated: 2011_08_17-PM-04_32_13
Last ObjectModification: 2011_06_18-AM-11_43_29

Home Index