---

{ [Info:Type]
    es:EO+(Info)
      [Qa,Rb,Sc:E  E  ]. [A,B,C:Type].
        Ia:EClass(A). Ib:EClass(B). Ic:EClass(C). f1:E(Ia)  B. f2:B  C.
          ((Ia:Qa f1  Ib:Rb  Ib:Rb e.(f2 Ib(e))  Ic:Sc)
           Ia:Qa f2 o f1  Ic:Sc) }

{ Proof }

---

Definitions occuring in Statement :  Q-R-glued: Ia:Qa f  Ib:Rb,  es-E-interface: E(X),  eclass-val: X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  compose: f o g,  uall: [x:A]. B[x],  prop: ,  all: x:A. B[x],  implies: P  Q,  and: P  Q,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  prop: ,  implies: P  Q,  and: P  Q,  Q-R-glued: Ia:Qa f  Ib:Rb,  cand: A c B,  member: t  T,  assert: b,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  exists: x:A. B[x],  es-E-interface: E(X),  so_apply: x[s1;s2],  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  subtype: S  T
Lemmas :  Q-R-glued_wf,  eclass-val_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  es-E-interface_wf,  eclass_wf,  assert_elim,  in-eclass_wf,  Q-R-glues-property,  es-interface-top,  compose_wf,  Q-R-glues_wf,  Q-R-glues-composes

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[Qa,Rb,Sc:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B,C:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}Ic:EClass(C).  \mforall{}f1:E(Ia)  {}\mrightarrow{}  B.  \mforall{}f2:B  {}\mrightarrow{}  C.
                ((Ia:Qa  \mrightarrow{}{}f1{}\mrightarrow{}    Ib:Rb  \mwedge{}  Ib:Rb  \mrightarrow{}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}    Ic:Sc)  {}\mRightarrow{}  Ia:Qa  \mrightarrow{}{}f2  o  f1{}\mrightarrow{}    Ic:Sc)


Date html generated: 2011_08_16-PM-05_59_58
Last ObjectModification: 2011_06_20-AM-01_42_10

Home Index