---

{ A,B:ValueAllType'.
    [X:EClass(A)]. [Y:A  EClass'(B)].
      (NormalLProgrammable'(A;X)
       (a:A. NormalLProgrammable'(B;Y[a]))
       NormalLProgrammable'(B;X >a> Y[a])) }

{ Proof }

---

Definitions occuring in Statement :  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  bind-class: X >x> Y[x],  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x],  vatype: ValueAllType
Lemmas :  valueall-type_wf,  Message-inhabited,  squash_wf,  bind-class-locally-programmable,  event-ordering+_inc,  event-ordering+_wf,  es-E_wf,  bag_wf,  intensional-universe_wf,  uall_wf,  eclass_wf2,  eclass_wf3,  subtype_rel_wf,  member_wf,  vatype_wf,  eclass_wf,  normal-locally-programmable_wf,  local-program-at_wf,  Id_wf,  Message_wf,  dataflow-program_wf

---

\mforall{}A,B:ValueAllType'.
    \mforall{}[X:EClass(A)].  \mforall{}[Y:A  {}\mrightarrow{}  EClass'(B)].
        (NormalLProgrammable'(A;X)
        {}\mRightarrow{}  (\mforall{}a:A.  NormalLProgrammable'(B;Y[a]))
        {}\mRightarrow{}  NormalLProgrammable'(B;X  >a>  Y[a]))


Date html generated: 2011_08_17-PM-04_12_05
Last ObjectModification: 2011_06_29-PM-08_58_00

Home Index