### Nuprl Lemma : filter-union

`∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ∀P:T ⟶ 𝔹.  (filter(P;as ⋃ bs) = filter(P;as) ⋃ filter(P;bs) ∈ (T List))`

Proof

Definitions occuring in Statement :  l-union: `as ⋃ bs` filter: `filter(P;l)` list: `T List` deq: `EqDecider(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` l-union: `as ⋃ bs` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` prop: `ℙ` uimplies: `b supposing a` implies: `P `` Q` top: `Top` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` squash: `↓T` not: `¬A` iff: `P `⇐⇒` Q` true: `True` rev_implies: `P `` Q` cand: `A c∧ B`
Lemmas referenced :  list_induction equal_wf list_wf filter_wf5 reduce_wf insert_wf subtype_rel_dep_function bool_wf l_member_wf subtype_rel_self set_wf reduce_nil_lemma filter_nil_lemma reduce_cons_lemma filter_cons_lemma eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot deq_wf insert-cases2 squash_wf true_wf ite_rw_false cons_wf member_filter_2 assert_wf iff_weakening_equal member_filter
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis because_Cache applyEquality setEquality independent_isectElimination setElimination rename independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality functionExtensionality unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination dependent_pairFormation promote_hyp instantiate functionEquality axiomEquality universeEquality hyp_replacement applyLambdaEquality imageElimination equalityUniverse levelHypothesis natural_numberEquality imageMemberEquality baseClosed independent_pairFormation

Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.    (filter(P;as  \mcup{}  bs)  =  filter(P;as)  \mcup{}  filter(P;bs))

Date html generated: 2017_04_17-AM-09_09_50
Last ObjectModification: 2017_02_27-PM-05_17_56

Theory : decidable!equality

Home Index