---

{ [Info:Type]
    es:EO+(Info)
      [Q1,Q2,R:E  E  ]. [A,B:Type].
        Ia1,Ia2:EClass(A). Ib1,Ib2:EClass(B). f:E([Ia1?Ia2])  B. g1:E(Ib1)
                                                                           E.
        g2:E(Ib2)  E.
          (g1 glues Ia1:Q1 f Ib1:R
              g2 glues Ia2:Q2 f Ib2:R
              [{Ib1}? g1 : g2] glues [Ia1?Ia2]:Q1|{Ia1}  Q2|{Ia2} f 
                [Ib1?Ib2]:R) supposing 
             (Ib1  Ib2 = 0 and 
             Ia1  Ia2 = 0) }

{ Proof }

---

Definitions occuring in Statement :  Q-R-glues: g glues Ia:Qa f Ib:Rb,  es-interface-disjoint: X  Y = 0,  es-E-interface: E(X),  es-interface-predicate: {I},  cond-class: [X?Y],  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  conditional: [P? f : g],  es-E: E,  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  all: x:A. B[x],  implies: P  Q,  lambda: x.A[x],  function: x:A  B[x],  universe: Type,  rel_or: R1  R2,  rel-restriction: R|P,  bool-decider: bool-decider(b)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  prop: ,  uimplies: b supposing a,  es-interface-disjoint: X  Y = 0,  implies: P  Q,  member: t  T,  not: A,  and: P  Q,  false: False,  so_lambda: x y.t[x; y],  so_apply: x[s1;s2],  subtype: S  T
Lemmas :  assert_wf,  in-eclass_wf,  es-E_wf,  event-ordering+_inc,  Q-R-glues-conditional,  Q-R-glues_wf,  subtype_rel_function,  es-E-interface_wf,  cond-class_wf,  top_wf,  es-E-interface-conditional-subtype2,  subtype_rel_self,  es-E-interface-conditional-subtype1,  es-interface-disjoint_wf,  es-interface-top,  eclass_wf,  event-ordering+_wf,  Q-R-glues-property

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[Q1,Q2,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
            \mforall{}Ia1,Ia2:EClass(A).  \mforall{}Ib1,Ib2:EClass(B).  \mforall{}f:E([Ia1?Ia2])  {}\mrightarrow{}  B.  \mforall{}g1:E(Ib1)  {}\mrightarrow{}  E.
            \mforall{}g2:E(Ib2)  {}\mrightarrow{}  E.
                (g1  glues  Ia1:Q1  {}{}f{}\mrightarrow{}  Ib1:R
                      {}\mRightarrow{}  g2  glues  Ia2:Q2  {}{}f{}\mrightarrow{}  Ib2:R
                      {}\mRightarrow{}  [\{Ib1\}?  g1  :  g2]  glues  [Ia1?Ia2]:Q1|\{Ia1\}  \mvee{}  Q2|\{Ia2\}  {}{}f{}\mrightarrow{}  [Ib1?Ib2]:R)  supposing 
                      (Ib1  \mcap{}  Ib2  =  0  and 
                      Ia1  \mcap{}  Ia2  =  0)


Date html generated: 2011_08_16-PM-05_58_29
Last ObjectModification: 2011_06_20-AM-01_41_10

Home Index