---

{ [A:']
    B:{B:'| valueall-type(B)} . F:Id  bag(A)  bag(B).
      [X:EClass(A)]
        NormalLProgrammable'(A;X)
         NormalLProgrammable'(B;simple-loc-comb1(l,a.F[l;a];X)) 
        supposing l:Id. (F[l;{}] = {}) }

{ Proof }

---

Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  simple-loc-comb1: simple-loc-comb1(l,b.F[l; b];X),  eclass: EClass(A[eo; e]),  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  all: x:A. B[x],  implies: 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 :  length_wf1,  int_subtype_base,  subtype_base_sq,  decidable__equal_int,  select_wf,  int_seg_wf,  nat_wf,  false_wf,  not_wf,  le_wf,  Message-inhabited,  subtype_rel_wf,  squash_wf,  simple-loc-comb-locally-programmable1,  event-ordering+_inc,  event-ordering+_wf,  es-E_wf,  sq_stable_from_decidable,  sq_stable__uall,  sq_stable__all,  uall_wf,  member_wf,  eclass_wf2,  eclass_wf3,  empty-bag_wf,  valueall-type_wf,  eclass_wf,  bag_wf,  normal-locally-programmable_wf,  dataflow-program_wf,  simple-loc-comb1_wf,  Message_wf,  local-program-at_wf,  Id_wf

---

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


Date html generated: 2011_08_17-PM-04_08_10
Last ObjectModification: 2011_06_29-PM-06_17_46

Home Index