---

{ [A:']
    B:{B:'| valueall-type(B)} . F:bag(A)  bag(B).
      [X:EClass(A)]
        NormalLProgrammable'(A;X)  NormalLProgrammable'(B;F|X|) 
        supposing (F {}) = {} }

{ Proof }

---

Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  simple-comb-1: F|X|,  eclass: EClass(A[eo; e]),  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t,  empty-bag: {},  bag: bag(T),  valueall-type: valueall-type(T)
Lemmas :  simple-comb1-nlp

---

\mforall{}[A:\mBbbU{}']
    \mforall{}B:\{B:\mBbbU{}'|  valueall-type(B)\}  .  \mforall{}F:bag(A)  {}\mrightarrow{}  bag(B).
        \mforall{}[X:EClass(A)].  NormalLProgrammable'(A;X)  {}\mRightarrow{}  NormalLProgrammable'(B;F|X|)  supposing  (F  \{\})  =  \{\}


Date html generated: 2011_08_17-PM-04_08_02
Last ObjectModification: 2011_06_29-PM-06_17_30

Home Index