{ 
[dv:ClassDerivation]
(fst(Meaning(dv))) = hd(cdv-types(dv)) supposing WF(dv) }
{ Proof }
Definitions occuring in Statement :
cdv-meaning: Meaning(dv),
cdv-wf: WF(dv),
cdv-types: cdv-types(dv),
classderiv: ClassDerivation,
hd: hd(l),
uimplies: b supposing a,
uall: [x:A]. B[x],
pi1: fst(t),
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
pi1: fst(t),
cdv-meaning: Meaning(dv),
hd: hd(l),
cdv-types: cdv-types(dv),
member: t 
T,
cdv-classes-and-programs: cdv-classes-and-programs(dv),
implies: P 
Q,
all: x:A. B[x],
top: Top,
subtype: S 
T,
prop: 
,
le: A 
B,
ge: i 
j ,
not: 
A,
false: False,
append: as @ bs,
map: map(f;as),
ycomb: Y,
spreadn: spread3,
classderiv: ClassDerivation,
cdv-wf: WF(dv),
unit: Unit,
and: P 
Q,
length: ||as||,
nat: 
,
cdv-class-program: ClassProgram,
cdvbase: cdvbase(args),
cdvpair: cdvpair(fst;snd),
it: 
,
cdvdelay: cdvdelay(X;dummy),
cdvcomb: cdvcomb(typ;argtype;arg;fun),
cdvreccomb: cdvreccomb(typ;argtype;arg;fun)
Lemmas :
classderiv_wf,
base-deriv-type_wf,
cdv-wf_wf,
cdvbase_wf,
cdvcomb_wf,
cdvreccomb_wf,
cdv-classes-and-programs_wf,
cdv-class-program_wf,
cdv-classes-non-null,
length_wf_nat,
top_wf,
nat_wf,
length_wf1,
member_wf,
pi1_wf_top,
hd_wf,
length_wf2,
cdv-types_wf,
cdv-types-non-empty,
ge_wf
\mforall{}[dv:ClassDerivation]. (fst(Meaning(dv))) = hd(cdv-types(dv)) supposing WF(dv)
Date html generated:
2011_08_17-PM-04_28_54
Last ObjectModification:
2011_06_18-AM-11_41_39
Home
Index