{ 
[dv:ClassDerivation]. 0 < ||cdv-classes-and-programs(dv)|| supposing WF(dv) }
{ Proof }
Definitions occuring in Statement :
cdv-classes-and-programs: cdv-classes-and-programs(dv),
cdv-wf: WF(dv),
classderiv: ClassDerivation,
length: ||as||,
uimplies: b supposing a,
uall: [x:A]. B[x],
less_than: a < b,
natural_number: $n
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
cdv-wf: WF(dv),
length: ||as||,
cdv-classes-and-programs: cdv-classes-and-programs(dv),
member: t 
T,
top: Top,
and: P 
Q,
cdv-argtype: cdv-argtype(dv),
ycomb: Y,
prop: 
,
cand: A c B,
let: let,
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
all: x:A. B[x],
subtype: S 
T,
classderiv: ClassDerivation,
unit: Unit,
int_seg: {i..j
},
lelt: i j < k,
cdvbase: cdvbase(args),
it: 
,
cdvpair: cdvpair(fst;snd),
cdvdelay: cdvdelay(X;dummy),
cdvcomb: cdvcomb(typ;argtype;arg;fun),
cdvreccomb: cdvreccomb(typ;argtype;arg;fun)
Lemmas :
classderiv_wf,
true_wf,
cdv-wf_wf,
length-map,
cdv-class-program_wf,
cdv-classes-and-programs_wf,
cdv-argtype_wf,
top_wf,
select_wf,
cdv-types_wf,
int_seg_wf,
length_wf1,
subtype_rel_weakening,
ext-eq_weakening,
length-append,
non_neg_length,
length_wf_nat
\mforall{}[dv:ClassDerivation]. 0 < ||cdv-classes-and-programs(dv)|| supposing WF(dv)
Date html generated:
2011_08_17-PM-04_28_34
Last ObjectModification:
2011_06_18-AM-11_41_15
Home
Index