Nuprl Lemma : Q-R-glues-conditional2

    ∀[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 and 
           Ia1 ∩ Ia2 0)


Definitions occuring in Statement :  Q-R-glues: glues Ia:Qa ──f─→ Ib:Rb es-interface-disjoint: X ∩ 0 es-E-interface: E(X) es-interface-predicate: {I} cond-class: [X?Y] in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) conditional: [P? g] es-E: E rel-restriction: R|P rel_or: R1 ∨ R2 uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] implies:  Q lambda: λx.A[x] function: x:A ─→ B[x] universe: Type bool-decider: bool-decider(b)
Lemmas :  assert_wf in-eclass_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype event-ordering+_wf top_wf Q-R-glues-conditional Q-R-glues-property Q-R-glues_wf subtype_rel_dep_function es-E-interface_wf cond-class_wf es-E-interface-conditional-subtype2 es-E-interface-conditional-subtype1 es-interface-disjoint_wf eclass_wf

        \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: 2015_07_21-PM-04_10_43
Last ObjectModification: 2015_01_27-PM-05_42_48

Home Index