{ 
[d:ClassDerivation]. (WF(d) 
') }
{ Proof }
Definitions occuring in Statement :
cdv-wf: WF(dv),
classderiv: ClassDerivation,
uall: [x:A]. B[x],
prop: ,
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
prop: ,
cdv-wf: WF(dv),
and: P 
Q,
cdv-argtype: cdv-argtype(dv),
top: Top,
so_lambda: 
x.t[x],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
cand: A c B,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
let: let,
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
so_apply: x[s],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2;s3;s4;s5],
int_seg: {i..j
},
uimplies: b supposing a,
lelt: i j < k
Lemmas :
classderiv_ind_wf,
true_wf,
base-deriv_wf,
classderiv_wf,
unit_wf,
cdv-argtype_wf,
top_wf,
select_wf,
cdv-types_wf,
int_seg_wf,
length_wf1,
subtype_rel_weakening,
ext-eq_weakening
\mforall{}[d:ClassDerivation]. (WF(d) \mmember{} \mBbbP{}')
Date html generated:
2011_08_17-PM-04_27_34
Last ObjectModification:
2010_11_12-AM-05_53_42
Home
Index