---

{ [Info:{Info:Type| Info} ]
    A:Type. locs:bag(Id).
      [X:EClass(A)]
        Xpr:NormalLProgrammable(A;X)
          (at-prc(A;Xpr;locs)  NormalLProgrammable(A;X@locs)) }

{ Proof }

---

Definitions occuring in Statement :  at-prc: at-prc(A;Xpr;locs),  normal-locally-programmable: NormalLProgrammable(A;X),  class-at: X@locs,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  all: x:A. B[x],  squash: T,  member: t  T,  set: {x:A| B[x]} ,  universe: Type,  bag: bag(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  member: t  T,  at-prc: at-prc(A;Xpr;locs),  ifthenelse: if b then t else f fi ,  bag-deq-member: bag-deq-member(eq;x;b),  id-deq: IdDeq,  null-df-program: null-df-program(B),  class-at-locally-programmable,  bfalse: ff,  bor: p q,  eqof: eqof(d),  deq-member: deq-member(eq;x;L),  reduce: reduce(f;k;as),  it: ,  btrue: tt,  atom2-deq: Atom2Deq,  eq_atom: eq_atom$n(x;y),  unit: Unit,  empty-bag: {},  implies: P  Q,  prop: ,  so_lambda: x.t[x],  so_lambda: x y.t[x; y],  so_apply: x[s],  so_apply: x[s1;s2],  subtype: S  T
Lemmas :  uall_wf,  squash_wf,  bag_wf,  Id_wf,  eclass_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  normal-locally-programmable_wf,  class-at_wf

---

\mforall{}[Info:\{Info:Type|  \mdownarrow{}Info\}  ]
    \mforall{}A:Type.  \mforall{}locs:bag(Id).
        \mforall{}[X:EClass(A)]
            \mforall{}Xpr:NormalLProgrammable(A;X).  (at-prc(A;Xpr;locs)  \mmember{}  NormalLProgrammable(A;X@locs))


Date html generated: 2011_08_16-PM-06_33_35
Last ObjectModification: 2011_08_13-PM-09_28_13

Home Index