{ 
[bdv:BaseDef]. (base-deriv-program(bdv) 
eclass-program{i:l}(Message)) }
{ Proof }
Definitions occuring in Statement :
base-deriv-program: base-deriv-program(bdv),
base-deriv: BaseDef,
Message: Message,
eclass-program: eclass-program{i:l}(Info),
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
Message: Message,
base-deriv-program: base-deriv-program(bdv),
pMsg: pMsg(P.M[P]),
mData: mData,
spreadn: spread4,
base-deriv: BaseDef
Lemmas :
base-program_wf,
base-deriv_wf
\mforall{}[bdv:BaseDef]. (base-deriv-program(bdv) \mmember{} eclass-program\{i:l\}(Message))
Date html generated:
2011_08_17-PM-04_22_16
Last ObjectModification:
2010_11_12-AM-05_42_55
Home
Index