{ 
[L:{dv:ClassDerivation| WF(dv)} List
]
(cdv-types(list-to-cdv(L)) ~ concat(map(
dv.cdv-types(dv);L))) }
{ Proof }
Definitions occuring in Statement :
list-to-cdv: list-to-cdv(L),
cdv-wf: WF(dv),
cdv-types: cdv-types(dv),
classderiv: ClassDerivation,
map: map(f;as),
uall: [x:A]. B[x],
set: {x:A| B[x]} ,
lambda: x.A[x],
sqequal: s ~ t,
listp: A List,
concat: concat(ll)
Definitions :
uall: [x:A]. B[x],
list-to-cdv: list-to-cdv(L),
map: map(f;as),
member: t 
T,
ycomb: Y,
all: x:A. B[x],
list_accum: list_accum(x,a.f[x; a];y;l),
hd: hd(l),
tl: tl(l),
top: Top,
subtype: S 
T,
cdv-wf: WF(dv),
and: P 
Q,
cdv-types: cdv-types(dv),
listp: A List,
ge: i 
j ,
length: ||as||,
prop: 
,
le: A 
B,
not: 
A,
implies: P 
Q,
false: False
Lemmas :
listp_properties,
classderiv_wf,
cdv-wf_wf,
concat-single,
cdv-types_wf,
top_wf,
concat-cons,
map_wf,
listp_wf,
cdvpair_wf,
append_assoc_sq
\mforall{}[L:\{dv:ClassDerivation| WF(dv)\} List\msupplus{}]
(cdv-types(list-to-cdv(L)) \msim{} concat(map(\mlambda{}dv.cdv-types(dv);L)))
Date html generated:
2011_08_17-PM-04_27_52
Last ObjectModification:
2011_06_18-AM-11_41_02
Home
Index