### Nuprl Lemma : remove-repeats-fun-map

`∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List].`
`  (map(f;remove-repeats-fun(eq;f;L)) = remove-repeats(eq;map(f;L)) ∈ (B List))`

Proof

Definitions occuring in Statement :  remove-repeats-fun: `remove-repeats-fun(eq;f;L)` remove-repeats: `remove-repeats(eq;L)` map: `map(f;as)` list: `T List` deq: `EqDecider(T)` uall: `∀[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` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` remove-repeats-fun: `remove-repeats-fun(eq;f;L)` all: `∀x:A. B[x]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` squash: `↓T` true: `True` prop: `ℙ` deq: `EqDecider(T)` compose: `f o g` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction equal_wf list_wf map_wf remove-repeats-fun_wf remove-repeats_wf list_ind_nil_lemma map_nil_lemma remove_repeats_nil_lemma nil_wf list_ind_cons_lemma map_cons_lemma remove_repeats_cons_lemma cons_wf deq_wf filter_wf5 l_member_wf bnot_wf set_wf filter-map squash_wf true_wf bool_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis functionExtensionality applyEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation rename imageElimination because_Cache natural_numberEquality imageMemberEquality baseClosed axiomEquality functionEquality universeEquality equalityUniverse levelHypothesis setElimination setEquality equalityTransitivity equalitySymmetry independent_isectElimination productElimination

Latex:
\mforall{}[A,B:Type].  \mforall{}[eq:EqDecider(B)].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[L:A  List].
(map(f;remove-repeats-fun(eq;f;L))  =  remove-repeats(eq;map(f;L)))

Date html generated: 2017_04_17-AM-09_12_11
Last ObjectModification: 2017_02_27-PM-05_19_27

Theory : decidable!equality

Home Index