{ 
[hdr:Name]. [locs:bag(Id)]. [T:Type]. (Base(hdr;locs;T) 
EClass'(T)) }
{ Proof }
Definitions occuring in Statement :
base-headers-msg-val-loc: Base(hdr;locs;typ),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
name: Name,
uall: [x:A]. B[x],
member: t T,
universe: Type,
bag: bag(T)
Lemmas :
bag_wf,
Id_wf,
name_wf,
class-at_wf,
Message_wf,
base-headers-msg-val_wf
\mforall{}[hdr:Name]. \mforall{}[locs:bag(Id)]. \mforall{}[T:Type]. (Base(hdr;locs;T) \mmember{} EClass'(T))
Date html generated:
2011_08_17-PM-04_02_11
Last ObjectModification:
2011_06_21-PM-04_28_32
Home
Index