### Nuprl Lemma : agree_on_common_filter

`∀[T:Type]. ∀P:T ⟶ 𝔹. ∀as,bs:T List.  (agree_on_common(T;as;bs) `` agree_on_common(T;filter(P;as);filter(P;bs)))`

Proof

Definitions occuring in Statement :  agree_on_common: `agree_on_common(T;as;bs)` filter: `filter(P;l)` list: `T List` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` so_apply: `x[s]` uimplies: `b supposing a` istype: `istype(T)` top: `Top` agree_on_common: `agree_on_common(T;as;bs)` list_ind: list_ind nil: `[]` it: `⋅` true: `True` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` or: `P ∨ Q` so_apply: `x[s1;s2;s3]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` bool: `𝔹` unit: `Unit` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` false: `False` not: `¬A` guard: `{T}`
Lemmas referenced :  list_induction all_wf list_wf agree_on_common_wf filter_wf5 subtype_rel_dep_function bool_wf istype-universe l_member_wf filter_nil_lemma istype-void nil_wf set_wf subtype_rel_self cons_wf ifthenelse_wf agree_on_common_nil filter_cons_lemma list_ind_cons_lemma not_wf bnot_wf assert_wf equal-wf-T-base eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot equal_wf agree_on_common_cons2 member_filter agree_on_common_cons
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality_alt hypothesis functionEquality because_Cache applyEquality setEquality setElimination rename setIsType universeIsType independent_isectElimination inhabitedIsType independent_functionElimination functionIsType dependent_functionElimination universeEquality isect_memberEquality_alt voidElimination lambdaEquality lambdaFormation natural_numberEquality productElimination voidEquality isect_memberEquality unionElimination baseClosed equalitySymmetry equalityTransitivity equalityElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T:Type]
\mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}as,bs:T  List.
(agree\_on\_common(T;as;bs)  {}\mRightarrow{}  agree\_on\_common(T;filter(P;as);filter(P;bs)))

Date html generated: 2019_10_15-AM-10_53_38
Last ObjectModification: 2018_10_09-AM-10_28_53

Theory : list!

Home Index