{ 
hdr:Name. locs:bag(Id). T:{T:Type| valueall-type(T)} .
NormalLProgrammable'(T;Base(hdr;locs;T)) }
{ Proof }
Definitions occuring in Statement :
base-headers-msg-val-loc: Base(hdr;locs;typ),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
Id: Id,
name: Name,
all: x:A. B[x],
set: {x:A| B[x]} ,
universe: Type,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
all: x:A. B[x],
member: t 
T,
uall: [x:A]. B[x]
Lemmas :
base-at-prc_wf,
valueall-type_wf,
bag_wf,
Id_wf,
name_wf
\mforall{}hdr:Name. \mforall{}locs:bag(Id). \mforall{}T:\{T:Type| valueall-type(T)\} . NormalLProgrammable'(T;Base(hdr;locs;T))
Date html generated:
2011_08_17-PM-04_02_18
Last ObjectModification:
2011_08_13-PM-10_55_08
Home
Index