### Nuprl Lemma : filter-list-diff

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List]. ∀[eq:EqDecider(T)].  (filter(P;L1-L2) ~ filter(P;L1)-filter(P;L2))`

Proof

Definitions occuring in Statement :  list-diff: `as-bs` filter: `filter(P;l)` list: `T List` deq: `EqDecider(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` function: `x:A ⟶ B[x]` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  list-diff: `as-bs` top: `Top` member: `t ∈ T` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` prop: `ℙ` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` bfalse: `ff` false: `False` not: `¬A` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B`
Lemmas referenced :  filter-sq l_member_wf bnot_wf deq-member_wf bool_wf eqtt_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base eqff_to_assert assert-bnot assert-deq-member filter_wf5 subtype_rel_dep_function subtype_rel_self set_wf assert_witness assert_wf not_wf member_filter_2 iff_wf band_wf bfalse_wf assert_elim and_wf btrue_neq_bfalse deq_wf list_wf filter-filter iff_transitivity iff_weakening_uiff assert_of_band assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberEquality voidElimination voidEquality sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality lambdaFormation cumulativity hypothesis setElimination rename unionElimination equalityElimination productElimination independent_isectElimination because_Cache dependent_pairFormation equalityTransitivity equalitySymmetry promote_hyp dependent_functionElimination instantiate independent_functionElimination applyEquality functionExtensionality setEquality independent_pairFormation productEquality addLevel impliesFunctionality andLevelFunctionality impliesLevelFunctionality levelHypothesis dependent_set_memberEquality applyLambdaEquality functionEquality universeEquality isect_memberFormation sqequalAxiom

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L1,L2:T  List].  \mforall{}[eq:EqDecider(T)].
(filter(P;L1-L2)  \msim{}  filter(P;L1)-filter(P;L2))

Date html generated: 2017_04_17-AM-09_14_58
Last ObjectModification: 2017_02_27-PM-05_20_51

Theory : decidable!equality

Home Index