---

{ [c:CombinatorDef]
    (mk-combdef(c)  BaseDef + CombinatorDef + {dv:ClassDerivation| 
                                                WF(dv)
                                                 (||cdv-types(dv)|| = 1)} ) }

{ Proof }

---

Definitions occuring in Statement :  mk-combdef: mk-combdef(c),  combinator-def: CombinatorDef,  cdv-wf: WF(dv),  cdv-types: cdv-types(dv),  classderiv: ClassDerivation,  base-deriv: BaseDef,  length: ||as||,  uall: [x:A]. B[x],  and: P  Q,  member: t  T,  set: {x:A| B[x]} ,  union: left + right,  natural_number: $n,  int: ,  equal: s = t
Definitions :  uall: [x:A]. B[x],  member: t  T,  and: P  Q,  mk-combdef: mk-combdef(c),  prop:
Lemmas :  classderiv_wf,  cdv-wf_wf,  length_wf1,  cdv-types_wf,  base-deriv_wf,  combinator-def_wf

---

\mforall{}[c:CombinatorDef]
    (mk-combdef(c)  \mmember{}  BaseDef  +  CombinatorDef  +  \{dv:ClassDerivation|  WF(dv)  \mwedge{}  (||cdv-types(dv)||  =  1)\}  \000C)


Date html generated: 2011_08_17-PM-06_30_55
Last ObjectModification: 2011_06_18-AM-11_53_26

Home Index