---

{ [Info:{Info:Type| Info} ]
    A:{T:Type| valueall-type(T)} 
      [X:EClass(A)]
        (NormalLProgrammable(A;X)  NormalLProgrammable(A;Prior(X))) }

{ Proof }

---

Definitions occuring in Statement :  normal-locally-programmable: NormalLProgrammable(A;X),  primed-class: Prior(X),  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  all: x:A. B[x],  squash: T,  implies: P  Q,  set: {x:A| B[x]} ,  universe: Type,  valueall-type: valueall-type(T)
Lemmas :  primed-class-opt-locally-programmable,  squash_wf,  valueall-type_wf,  uall_wf,  eclass_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  primed-class_wf,  local-program-at_wf,  dataflow-program_wf,  normal-locally-programmable_wf,  empty-bag_wf,  Id_wf

---

\mforall{}[Info:\{Info:Type|  \mdownarrow{}Info\}  ]
    \mforall{}A:\{T:Type|  valueall-type(T)\} 
        \mforall{}[X:EClass(A)].  (NormalLProgrammable(A;X)  {}\mRightarrow{}  NormalLProgrammable(A;Prior(X)))


Date html generated: 2011_08_16-PM-06_19_36
Last ObjectModification: 2011_07_25-PM-05_15_03

Home Index