Nuprl Lemma : agree_on_common_append

`∀[T:Type]`
`  ∀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)))`

Proof

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: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  so_apply: `x[s1;s2;s3]` top: `Top` so_lambda: so_lambda3 append: `as @ bs` implies: `P `` Q` so_apply: `x[s]` prop: `ℙ` uimplies: `b 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 ⊆r B` true: `True` agree_on_common: `agree_on_common(T;as;bs)` and: `P ∧ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` or: `P ∨ Q` exists: `∃x:A. B[x]` l_member: `(x ∈ l)` cand: `A 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

Latex:
\mforall{}[T:Type]
\mforall{}as,bs,cs,ds:T  List.
(agree\_on\_common(T;as;cs)
{}\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