---

{ [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.
        g1:E(Ib)  E. g2:E(Ic)  E.
          ((g1 glues Ia:Qa f1 Ib:Rb
           g2 glues Ib:Rb e.(f2 Ib(e)) Ic:Sc)
           g1 o g2 glues Ia:Qa f2 o f1 Ic:Sc) }

{ Proof }

---

Definitions occuring in Statement :  Q-R-glues: g glues 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,  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,  es-E-interface: E(X),  uimplies: b supposing a,  so_apply: x[s1;s2],  sq_type: SQType(T),  guard: {T},  subtype: S  T
Lemmas :  Q-R-glues-composes,  Q-R-glues-property,  eclass-val_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  subtype_base_sq,  bool_subtype_base,  es-E-interface_wf,  Q-R-glues_wf,  bool_wf,  eclass_wf,  assert_elim,  in-eclass_wf

---

\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.  \mforall{}g1:E(Ib)  {}\mrightarrow{}  E.
            \mforall{}g2:E(Ic)  {}\mrightarrow{}  E.
                ((g1  glues  Ia:Qa  {}{}f1{}\mrightarrow{}  Ib:Rb  \mwedge{}  g2  glues  Ib:Rb  {}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}  Ic:Sc)
                {}\mRightarrow{}  g1  o  g2  glues  Ia:Qa  {}{}f2  o  f1{}\mrightarrow{}  Ic:Sc)


Date html generated: 2011_08_16-PM-05_58_02
Last ObjectModification: 2011_06_20-AM-01_40_52

Home Index