Nuprl Lemma : Q-R-glued-first

    ∀[Q,R:E ─→ E ─→ ℙ]. ∀[A,B:Type].
      ∀Ias:EClass(A) List. ∀Ibs:EClass(B) List. ∀f:E(first-class(Ias)) ─→ B.
        ((∀i:ℕ||Ias||. Ias[i]:Q →─f─→  Ibs[i]:R)
            first-class(Ias):Q →─f─→  first-class(Ibs):R 
              supposing (∀Ia1,Ia2∈Ias.  ∀e,e':E.
                                          ((¬(Q e')) ∧ (Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposi\000Cng 
           ((||Ias|| ||Ibs|| ∈ ℤand 
           (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 0) and 
           (∀Ia1,Ia2∈Ias.  Ia1 ∩ Ia2 0))


Definitions occuring in Statement :  Q-R-glued: Ia:Qa →─f─→  Ib:Rb es-interface-disjoint: X ∩ 0 es-E-interface: E(X) first-class: first-class(L) in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E pairwise: (∀x,y∈L.  P[x; y]) select: L[n] length: ||as|| list: List int_seg: {i..j-} assert: b uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q apply: a function: x:A ─→ B[x] natural_number: $n int: universe: Type equal: t ∈ T
Lemmas :  list_induction eclass_wf all_wf list_wf es-E_wf event-ordering+_subtype es-E-interface_wf first-class_wf top_wf subtype_rel_list es-interface-subtype_rel2 isect_wf pairwise_wf es-interface-disjoint_wf length_wf int_seg_wf Q-R-glued_wf select_wf sq_stable__le less_than_transitivity1 le_weakening subtype_rel_dep_function es-E-interface-first-class assert_wf in-eclass_wf not_wf event-ordering+_wf length_of_nil_lemma stuck-spread base_wf list-cases less_than_irreflexivity equal-wf-base product_subtype_list length_of_cons_lemma cons_wf length_cons non_neg_length length_wf_nat equal-wf-base-T nil_wf Q-R-glued-empty reduce_nil_lemma equal_wf le_weakening2 less_than_transitivity2 reduce_cons_lemma es-E-interface-conditional-subtype2 cond-class_wf pairwise-cons lelt_wf select_cons_tl_sq Q-R-glued-conditional subtype_rel_self l_all_iff l_member_wf l_exists_iff is-first-class or_wf es-interface-conditional-domain-iff decidable__assert Q-R-glues_functionality Q-R-glues_wf es-interface-predicate_wf rel-restriction_wf rel_or_wf

        \mforall{}[Q,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
            \mforall{}Ias:EClass(A)  List.  \mforall{}Ibs:EClass(B)  List.  \mforall{}f:E(first-class(Ias))  {}\mrightarrow{}  B.
                ((\mforall{}i:\mBbbN{}||Ias||.  Ias[i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:R)
                      {}\mRightarrow{}  first-class(Ias):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):R 
                            supposing  (\mforall{}Ia1,Ia2\mmember{}Ias.    \mforall{}e,e':E.
                                                                                    ((\mneg{}(Q  e  e'))  \mwedge{}  (\mneg{}(Q  e'  e)))  supposing 
                                                                                          ((\muparrow{}e'  \mmember{}\msubb{}  Ia2)  and 
                                                                                          (\muparrow{}e  \mmember{}\msubb{}  Ia1))))  supposing 
                      ((||Ias||  =  ||Ibs||)  and 
                      (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)  and 
                      (\mforall{}Ia1,Ia2\mmember{}Ias.    Ia1  \mcap{}  Ia2  =  0))

Date html generated: 2015_07_21-PM-04_13_22
Last ObjectModification: 2015_02_02-PM-06_44_51

Home Index