---

{ hdr:Name. locs:bag(Id). T:{T:Type| valueall-type(T)} .
    (base-at-prc(hdr;T;locs)  NormalLProgrammable'(T;Base(hdr;locs;T))) }

{ Proof }

---

Definitions occuring in Statement :  base-at-prc: base-at-prc(hdr;typ;locs),  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],  member: t  T,  set: {x:A| B[x]} ,  universe: Type,  bag: bag(T),  valueall-type: valueall-type(T)
Definitions :  all: x:A. B[x],  member: t  T,  base-headers-msg-val-loc: Base(hdr;locs;typ),  base-at-prc: base-at-prc(hdr;typ;locs),  prop: ,  name: Name,  squash: T,  Message: Message,  true: True,  pMsg: pMsg(P.M[P]),  mData: mData,  uall: [x:A]. B[x]
Lemmas :  valueall-type_wf,  bag_wf,  Id_wf,  name_wf,  at-prc_wf,  Message_wf,  squash_wf,  base-headers-msg-val_wf,  base-prc_wf,  int-valueall-type

---

\mforall{}hdr:Name.  \mforall{}locs:bag(Id).  \mforall{}T:\{T:Type|  valueall-type(T)\}  .
    (base-at-prc(hdr;T;locs)  \mmember{}  NormalLProgrammable'(T;Base(hdr;locs;T)))


Date html generated: 2011_08_17-PM-04_01_57
Last ObjectModification: 2011_08_13-PM-10_54_45

Home Index