---

{ [Info:{Info:Type| Info} ]
    A:{B:Type| valueall-type(B)} 
      [X:EClass(A)]
        Xpr:NormalLProgrammable(A;X)
          (once-prc(A;Xpr)  NormalLProgrammable(A;once-class(X))) }

{ Proof }

---

Definitions occuring in Statement :  once-prc: once-prc(A;Xpr),  normal-locally-programmable: NormalLProgrammable(A;X),  once-class: once-class(X),  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  all: x:A. B[x],  squash: T,  member: t  T,  set: {x:A| B[x]} ,  universe: Type,  valueall-type: valueall-type(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  member: t  T,  once-prc: once-prc(A;Xpr),  once-prog: once-prog(dfp),  once-class-locally-programmable,  evalall: evalall(t),  ifthenelse: if b then t else f fi ,  bag-null: bag-null(bs),  it: ,  spreadn: spread4,  btrue: tt,  bfalse: ff,  null: null(as),  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,  valueall-type_wf,  eclass_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  normal-locally-programmable_wf,  once-class_wf

---

\mforall{}[Info:\{Info:Type|  \mdownarrow{}Info\}  ]
    \mforall{}A:\{B:Type|  valueall-type(B)\} 
        \mforall{}[X:EClass(A)]
            \mforall{}Xpr:NormalLProgrammable(A;X).  (once-prc(A;Xpr)  \mmember{}  NormalLProgrammable(A;once-class(X)))


Date html generated: 2011_08_16-PM-06_33_07
Last ObjectModification: 2011_08_13-PM-09_19_03

Home Index