---

{ hdr:Name. T:{T:Type| valueall-type(T)} .
    NormalLProgrammable'(T;Base(hdr;T)) }

{ Proof }

---

Definitions occuring in Statement :  base-headers-msg-val: Base(hdr;typ),  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  name: Name,  all: x:A. B[x],  set: {x:A| B[x]} ,  universe: Type,  valueall-type: valueall-type(T)
Definitions :  all: x:A. B[x],  member: t  T,  uall: [x:A]. B[x]
Lemmas :  base-prc_wf,  valueall-type_wf,  name_wf

---

\mforall{}hdr:Name.  \mforall{}T:\{T:Type|  valueall-type(T)\}  .    NormalLProgrammable'(T;Base(hdr;T))


Date html generated: 2011_08_17-PM-04_02_04
Last ObjectModification: 2011_08_13-PM-10_50_24

Home Index