---

{ A:{A:'| valueall-type(A)} 
    [X:EClass(A)]
      init:Id  bag(A)
        (NormalLProgrammable'(A;X)  NormalLProgrammable'(A;Prior(X)?init)) }

{ Proof }

---

Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  primed-class-opt: Prior(X)?b,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  function: x:A  B[x],  universe: Type,  bag: bag(T),  valueall-type: valueall-type(T)
Lemmas :  normal-locally-programmable_wf,  Id_wf,  eclass_wf,  eclass_wf3,  eclass_wf2,  event-ordering+_wf,  es-E_wf,  event-ordering+_inc,  bag_wf,  valueall-type_wf,  primed-class-opt-locally-programmable,  member_wf,  subtype_rel_wf,  Message_wf,  squash_wf,  Message-inhabited

---

\mforall{}A:\{A:\mBbbU{}'|  valueall-type(A)\} 
    \mforall{}[X:EClass(A)]
        \mforall{}init:Id  {}\mrightarrow{}  bag(A).  (NormalLProgrammable'(A;X)  {}\mRightarrow{}  NormalLProgrammable'(A;Prior(X)?init))


Date html generated: 2011_08_17-PM-04_11_14
Last ObjectModification: 2011_07_22-PM-11_42_37

Home Index