{ 
[bdv:BaseDef]. (base-deriv-class(bdv) 
EClass'(base-deriv-type(bdv))) }
{ Proof }
Definitions occuring in Statement :
base-deriv-class: base-deriv-class(bdv),
base-deriv-type: base-deriv-type(bdv),
base-deriv: BaseDef,
Message: Message,
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
Message: Message,
base-deriv-type: base-deriv-type(bdv),
base-deriv-class: base-deriv-class(bdv),
spreadn: spread4,
pMsg: pMsg(P.M[P]),
base-deriv: BaseDef,
so_apply: x[s]
Lemmas :
restricted-baseclass_wf,
base-deriv_wf
\mforall{}[bdv:BaseDef]. (base-deriv-class(bdv) \mmember{} EClass'(base-deriv-type(bdv)))
Date html generated:
2011_08_17-PM-04_22_08
Last ObjectModification:
2010_11_12-AM-05_42_41
Home
Index