---

{ [Info:{Info:Type| Info} ]
    A,B:{B:Type| valueall-type(B)} .
      [X:EClass(A)]. [Y:EClass(B)].
        (NormalLProgrammable(A;X)
         NormalLProgrammable(B;Y)
         NormalLProgrammable(A;(X until Y))) }

{ Proof }

---

Definitions occuring in Statement :  normal-locally-programmable: NormalLProgrammable(A;X),  until-class: (X until Y),  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 :  isect_subtype_base,  squash_wf,  valueall-type_wf,  uall_wf,  eclass_wf,  normal-locally-programmable_wf,  until-class_wf,  subtype_base_sq,  until-class-lpg1

---

\mforall{}[Info:\{Info:Type|  \mdownarrow{}Info\}  ]
    \mforall{}A,B:\{B:Type|  valueall-type(B)\}  .
        \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
            (NormalLProgrammable(A;X)  {}\mRightarrow{}  NormalLProgrammable(B;Y)  {}\mRightarrow{}  NormalLProgrammable(A;(X  until  Y)))


Date html generated: 2011_08_16-PM-06_20_05
Last ObjectModification: 2011_06_29-PM-12_44_13

Home Index