---

{ [Info:{Info:Type| Info} ]
    A:{T:Type| valueall-type(T)} 
      [X:EClass(A)]
        init:Id  bag(A). Xpr:NormalLProgrammable(A;X).
          (prior-init-prc(A;Xpr;init)  NormalLProgrammable(A;Prior(X)?init)) }

{ Proof }

---

Definitions occuring in Statement :  prior-init-prc: prior-init-prc(A;Xpr;init),  normal-locally-programmable: NormalLProgrammable(A;X),  primed-class-opt: Prior(X)?b,  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]} ,  function: x:A  B[x],  universe: Type,  bag: bag(T),  valueall-type: valueall-type(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  bag: bag(T),  member: t  T,  prior-init-prc: prior-init-prc(A;Xpr;init),  delay-program: delay-program,  primed-class-opt-locally-programmable,  unit: Unit,  evalall: evalall(t),  let: let,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  bag-size: bag-size(bs),  band: p  q,  bnot: b,  isl: isl(x),  eq_int: (i = j),  it: ,  spreadn: spread4,  permutation: permutation(T;L1;L2),  int_seg: {i..j},  and: P  Q,  inject: Inj(A;B;f),  permute_list: (L o f),  exists: x:A. B[x],  lelt: i  j < k,  le: A  B,  false: False,  not: A,  implies: P  Q,  append: as @ bs,  select: l[i],  mklist: mklist(n;f),  le_int: i z j,  btrue: tt,  bfalse: ff,  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,  Id_wf,  bag_wf,  normal-locally-programmable_wf,  primed-class-opt_wf

---

\mforall{}[Info:\{Info:Type|  \mdownarrow{}Info\}  ]
    \mforall{}A:\{T:Type|  valueall-type(T)\} 
        \mforall{}[X:EClass(A)]
            \mforall{}init:Id  {}\mrightarrow{}  bag(A).  \mforall{}Xpr:NormalLProgrammable(A;X).
                (prior-init-prc(A;Xpr;init)  \mmember{}  NormalLProgrammable(A;Prior(X)?init))


Date html generated: 2011_08_16-PM-06_34_21
Last ObjectModification: 2011_08_13-PM-09_41_42

Home Index