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].
     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 


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: 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: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] set: {x:A| B[x]}  apply: a lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a mapfilter: mapfilter(f;P;L) squash: T prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt band: p ∧b q ifthenelse: if then else 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: ⇐⇒ Q rev_implies:  Q so_lambda: λ2y.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

\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].
          =  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 

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

Theory : decidable!equality

Home Index