### Nuprl Lemma : remove-repeats-mapfilter-with-fun

`∀[T,U:Type]. ∀[eq:EqDecider(U)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| ↑(P x)}  ⟶ U].`
`  (remove-repeats(eq;mapfilter(f;P;L))`
`     = mapfilter(f;λa.((P a) ∧b (¬b(∃x∈L.(P x) ∧b R[x;a] ∧b (eq (f x) (f a)))_b));L)`
`     ∈ (U List)) supposing `
`     (sorted-by(λx,y. (↑R[x;y]);L) and `
`     StAntiSym(T;x,y.↑R[x;y]) and `
`     Irrefl(T;x,y.↑R[x;y]))`

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` bl-exists: `(∃x∈L.P[x])_b` sorted-by: `sorted-by(R;L)` mapfilter: `mapfilter(f;P;L)` list: `T List` deq: `EqDecider(T)` irrefl: `Irrefl(T;x,y.E[x; y])` st_anti_sym: `StAntiSym(T;x,y.R[x; y])` band: `p ∧b q` bnot: `¬bb` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` set: `{x:A| B[x]} ` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` mapfilter: `mapfilter(f;P;L)` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` 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` so_apply: `x[s1;s2]` deq: `EqDecider(T)` bfalse: `ff` or: `P ∨ Q` assert: `↑b` true: `True` false: `False` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` irrefl: `Irrefl(T;x,y.E[x; y])` st_anti_sym: `StAntiSym(T;x,y.R[x; y])` top: `Top`
Lemmas referenced :  equal_wf squash_wf true_wf list_wf remove-repeats-fun-map2 filter_wf5 subtype_rel_dep_function bool_wf l_member_wf subtype_rel_self set_wf map_wf assert_wf eqtt_to_assert bnot_wf bl-exists_wf subtype_rel_sets bool_cases_sqequal filter_type iff_weakening_equal sorted-by_wf st_anti_sym_wf irrefl_wf deq_wf member_filter_2 remove-repeats-fun-as-filter sorted-by-filter filter-filter bl-exists-filter mapfilter_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache cumulativity sqequalRule setEquality independent_isectElimination setElimination rename lambdaFormation unionElimination equalityElimination productElimination functionExtensionality dependent_set_memberEquality dependent_functionElimination independent_functionElimination natural_numberEquality voidElimination imageMemberEquality baseClosed universeEquality isect_memberEquality axiomEquality functionEquality voidEquality

Latex:
\mforall{}[T,U:Type].  \mforall{}[eq:EqDecider(U)].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  U].
(remove-repeats(eq;mapfilter(f;P;L))
=  mapfilter(f;\mlambda{}a.((P  a)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(\mexists{}x\mmember{}L.(P  x)  \mwedge{}\msubb{}  R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b));L))  supposing
(sorted-by(\mlambda{}x,y.  (\muparrow{}R[x;y]);L)  and
StAntiSym(T;x,y.\muparrow{}R[x;y])  and
Irrefl(T;x,y.\muparrow{}R[x;y]))

Date html generated: 2017_04_17-AM-09_12_38
Last ObjectModification: 2017_02_27-PM-05_20_00

Theory : decidable!equality

Home Index