---

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

{ Proof }

---

Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  rec-combined-loc-class-opt-2: F|Loc, X, Y, Prior(self)?;init|,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  all: x:A. B[x],  squash: T,  implies: P  Q,  or: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  function: x:A  B[x],  universe: Type,  equal: s = t,  empty-bag: {},  bag: bag(T),  valueall-type: valueall-type(T)
Lemmas :  rec-combined-loc-class-opt-2_wf,  Message_wf,  Id_wf,  dataflow-program_wf,  local-program-at_wf,  normal-locally-programmable_wf,  squash_wf,  bag_wf,  eclass_wf,  valueall-type_wf,  empty-bag_wf,  eclass_wf3,  eclass_wf2,  member_wf,  uall_wf,  sq_stable__all,  sq_stable__uall,  sq_stable_from_decidable,  es-E_wf,  event-ordering+_wf,  event-ordering+_inc,  rec-comb-locally-programmable1,  subtype_rel_wf,  Message-inhabited,  le_wf,  not_wf,  false_wf,  nat_wf,  int_seg_wf,  select_wf,  int_seg_properties,  length_wf_nat,  length_nil,  length_cons,  non_neg_length,  length_wf1,  top_wf,  decidable__equal_int,  subtype_base_sq,  int_subtype_base,  decidable__or,  decidable__squash,  pos_length2

---

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


Date html generated: 2011_08_17-PM-04_10_51
Last ObjectModification: 2011_07_25-PM-05_55_39

Home Index