{ 
[dv:ClassDerivation]. Meaning(dv) 
ClassProgram supposing WF(dv) }
{ Proof }
Definitions occuring in Statement :
cdv-meaning: Meaning(dv),
cdv-class-program: ClassProgram,
cdv-wf: WF(dv),
classderiv: ClassDerivation,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t T,
cdv-meaning: Meaning(dv),
ge: i 
j ,
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
prop: 
Lemmas :
hd_wf,
cdv-class-program_wf,
cdv-classes-and-programs_wf,
cdv-classes-non-null,
length_wf1,
cdv-wf_wf,
classderiv_wf
\mforall{}[dv:ClassDerivation]. Meaning(dv) \mmember{} ClassProgram supposing WF(dv)
Date html generated:
2011_08_17-PM-04_28_43
Last ObjectModification:
2011_06_18-AM-11_41_27
Home
Index