---

{ A:ValueAllType'
    [X:EClass(A)]
      (NormalLProgrammable'(A;X)  NormalLProgrammable'(A;once-class(X))) }

{ Proof }

---

Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  once-class: once-class(X),  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  vatype: ValueAllType
Lemmas :  valueall-type_wf,  Message-inhabited,  normal-locally-programmable_wf,  event-ordering+_wf,  es-E_wf,  event-ordering+_inc,  bag_wf,  intensional-universe_wf,  subtype_rel_wf,  eclass_wf,  eclass_wf3,  eclass_wf2,  member_wf,  vatype_wf,  once-class-locally-programmable,  Message_wf,  squash_wf

---

\mforall{}A:ValueAllType'
    \mforall{}[X:EClass(A)].  (NormalLProgrammable'(A;X)  {}\mRightarrow{}  NormalLProgrammable'(A;once-class(X)))


Date html generated: 2011_08_17-PM-04_11_37
Last ObjectModification: 2011_06_29-PM-10_17_00

Home Index