---

{ [Info:{Info:Type| Info} ]
    B:{B:Type| valueall-type(B)} . n:.
      [A:n  Type]. [Xs:k:n  EClass(A k)].
        Xprs:k:n. NormalLProgrammable(A k;Xs k). F:Id
                                                        k:n  bag(A k)
                                                        bag(B).
          loc-comb2-prc(B;n;Xprs;F)  NormalLProgrammable(B;F|Loc; Xs|) 
          supposing i:Id
                      (((F i (i.{})) = {})
                       (f:k:n  bag(A k)
                           ((k:n. ((f k) = {}))  ((F i f) = {})))) }

{ Proof }

---

Definitions occuring in Statement :  loc-comb2-prc: loc-comb2-prc(T;n;Xs;F),  normal-locally-programmable: NormalLProgrammable(A;X),  simple-loc-comb: F|Loc; Xs|,  eclass: EClass(A[eo; e]),  Id: Id,  int_seg: {i..j},  nat: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  squash: T,  implies: P  Q,  and: P  Q,  member: t  T,  set: {x:A| B[x]} ,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  natural_number: $n,  universe: Type,  equal: s = t,  empty-bag: {},  bag: bag(T),  valueall-type: valueall-type(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  uimplies: b supposing a,  and: P  Q,  implies: P  Q,  exists: x:A. B[x],  member: t  T,  loc-comb2-prc: loc-comb2-prc(T;n;Xs;F),  upto: upto(n),  simple-loc-comb-locally-programmable2,  prop: ,  so_lambda: x.t[x],  so_lambda: x y.t[x; y],  cand: A c B,  nat: ,  so_apply: x[s],  so_apply: x[s1;s2],  subtype: S  T
Lemmas :  uall_wf,  squash_wf,  valueall-type_wf,  nat_wf,  int_seg_wf,  eclass_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  normal-locally-programmable_wf,  Id_wf,  bag_wf,  empty-bag_wf,  simple-loc-comb_wf,  nat_properties

---

\mforall{}[Info:\{Info:Type|  \mdownarrow{}Info\}  ]
    \mforall{}B:\{B:Type|  valueall-type(B)\}  .  \mforall{}n:\mBbbN{}.
        \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[Xs:k:\mBbbN{}n  {}\mrightarrow{}  EClass(A  k)].
            \mforall{}Xprs:\mforall{}k:\mBbbN{}n.  NormalLProgrammable(A  k;Xs  k).  \mforall{}F:Id  {}\mrightarrow{}  k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)  {}\mrightarrow{}  bag(B).
                loc-comb2-prc(B;n;Xprs;F)  \mmember{}  NormalLProgrammable(B;F|Loc;  Xs|) 
                supposing  \mforall{}i:Id
                                        (((F  i  (\mlambda{}i.\{\}))  =  \{\})
                                        \mwedge{}  (\mforall{}f:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k).  ((\mexists{}k:\mBbbN{}n.  ((f  k)  =  \{\}))  {}\mRightarrow{}  ((F  i  f)  =  \{\}))))


Date html generated: 2011_08_16-PM-06_34_50
Last ObjectModification: 2011_08_13-PM-09_13_50

Home Index