Nuprl Lemma : agree_on_common_append

  ∀as,bs,cs,ds:T List.
    (agree_on_common(T;as;cs)  agree_on_common(T;bs;ds)  agree_on_common(T;as bs;cs ds)) supposing 
       ((∀x∈as.¬(x ∈ ds)) and 
       (∀x∈cs.¬(x ∈ bs)))


Definitions occuring in Statement :  agree_on_common: agree_on_common(T;as;bs) l_all: (∀x∈L.P[x]) l_member: (x ∈ l) append: as bs list: List uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A implies:  Q universe: Type
Definitions unfolded in proof :  so_apply: x[s1;s2;s3] top: Top so_lambda: so_lambda3 append: as bs implies:  Q so_apply: x[s] prop: uimplies: supposing a so_lambda: λ2x.t[x] member: t ∈ T all: x:A. B[x] uall: [x:A]. B[x] false: False not: ¬A l_all: (∀x∈L.P[x]) subtype_rel: A ⊆B true: True agree_on_common: agree_on_common(T;as;bs) and: P ∧ Q iff: ⇐⇒ Q rev_implies:  Q or: P ∨ Q exists: x:A. B[x] l_member: (x ∈ l) cand: c∧ B
Lemmas referenced :  list_ind_cons_lemma istype-void list_ind_nil_lemma append_wf agree_on_common_wf not_wf istype-universe l_member_wf l_all_wf isect_wf list_wf all_wf list_induction cons_wf nil_wf l_all_wf_nil l_all_cons agree_on_common_cons2 agree_on_common_nil member_append cons_member
Rules used in proof :  universeEquality isectIsType functionIsType voidElimination isect_memberEquality_alt dependent_functionElimination independent_functionElimination inhabitedIsType functionEquality universeIsType setIsType rename setElimination because_Cache hypothesis lambdaEquality_alt sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution functionIsTypeImplies applyEquality natural_numberEquality productElimination independent_isectElimination inrFormation_alt equalityIsType1 unionIsType promote_hyp independent_pairFormation inlFormation_alt unionElimination productIsType equalityIstype

    \mforall{}as,bs,cs,ds:T  List.
              {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
              {}\mRightarrow{}  agree\_on\_common(T;as  @  bs;cs  @  ds))  supposing 
              ((\mforall{}x\mmember{}as.\mneg{}(x  \mmember{}  ds))  and 
              (\mforall{}x\mmember{}cs.\mneg{}(x  \mmember{}  bs)))

Date html generated: 2020_05_20-AM-07_48_15
Last ObjectModification: 2020_01_22-PM-05_26_07

Theory : list!

Home Index