---

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

{ Proof }

---

Definitions occuring in Statement :  glues: g glues Ia f Ib,  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],  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],  implies: P  Q,  and: P  Q,  glues: g glues Ia f Ib,  cand: A c B,  member: t  T,  prop: ,  assert: b,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  es-E-interface: E(X),  so_apply: x[s1;s2],  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  subtype: S  T
Lemmas :  glues_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,  es-le_wf,  Q-R-glues-composes,  glues-property,  es-interface-top

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \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.  \mforall{}g1:E(Ib)  {}\mrightarrow{}  E.
            \mforall{}g2:E(Ic)  {}\mrightarrow{}  E.
                ((g1  glues  Ia  {}{}f1{}\mrightarrow{}  Ib  \mwedge{}  g2  glues  Ib  {}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}  Ic)
                {}\mRightarrow{}  g1  o  g2  glues  Ia  {}{}f2  o  f1{}\mrightarrow{}  Ic)


Date html generated: 2011_08_16-PM-06_01_27
Last ObjectModification: 2011_06_20-AM-01_44_46

Home Index