---

{ [A,B:'].
    C:{C:'| valueall-type(C)} . F:Id  bag(A)  bag(B)  bag(C).
      [X:EClass(A)]. [Y:EClass(B)].
        (((l:Id
              ((as:bag(A). ((F l as {}) = {}))
               (bs:bag(B). ((F l {} bs) = {}))))
          (l:Id. ((F l {} {}) = {})))
         NormalLProgrammable'(A;X)
         NormalLProgrammable'(B;Y)
         NormalLProgrammable'(C;F|Loc,X, Y|)) }

{ Proof }

---

Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  simple-loc-comb-2: F|Loc,X, Y|,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  all: x:A. B[x],  squash: T,  implies: P  Q,  or: P  Q,  and: 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-loc-comb2-nlp

---

\mforall{}[A,B:\mBbbU{}'].
    \mforall{}C:\{C:\mBbbU{}'|  valueall-type(C)\}  .  \mforall{}F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C).
        \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
            (((\mdownarrow{}\mforall{}l:Id.  ((\mforall{}as:bag(A).  ((F  l  as  \{\})  =  \{\}))  \mwedge{}  (\mforall{}bs:bag(B).  ((F  l  \{\}  bs)  =  \{\}))))
              \mvee{}  (\mdownarrow{}\mforall{}l:Id.  ((F  l  \{\}  \{\})  =  \{\})))
            {}\mRightarrow{}  NormalLProgrammable'(A;X)
            {}\mRightarrow{}  NormalLProgrammable'(B;Y)
            {}\mRightarrow{}  NormalLProgrammable'(C;F|Loc,X,  Y|))


Date html generated: 2011_08_17-PM-04_09_39
Last ObjectModification: 2011_06_29-PM-10_56_34

Home Index