{ 
[x:BaseDef]
(mk-base(x) 
BaseDef + CombinatorDef + {dv:ClassDerivation|
WF(dv)
(||cdv-types(dv)|| = 1)} ) }
{ Proof }
Definitions occuring in Statement :
mk-base: mk-base(x),
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-base: mk-base(x),
prop: 
Lemmas :
combinator-def_wf,
classderiv_wf,
cdv-wf_wf,
length_wf1,
cdv-types_wf,
base-deriv_wf
\mforall{}[x:BaseDef]
(mk-base(x) \mmember{} BaseDef + CombinatorDef + \{dv:ClassDerivation| WF(dv) \mwedge{} (||cdv-types(dv)|| = 1)\} )
Date html generated:
2011_08_17-PM-06_30_46
Last ObjectModification:
2011_06_18-AM-11_53_11
Home
Index