### Nuprl Lemma : remove-repeats-fun-as-remove-repeats-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` all: `∀x:A. B[x]` top: `Top` remove-repeats-fun: `remove-repeats-fun(eq;f;L)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` squash: `↓T` compose: `f o g` prop: `ℙ` deq: `EqDecider(T)` true: `True`
Lemmas referenced :  list_induction equal_wf list_wf map_wf remove-repeats-fun_wf remove-repeats_wf map_nil_lemma remove_repeats_nil_lemma list_ind_nil_lemma nil_wf map_cons_lemma remove_repeats_cons_lemma list_ind_cons_lemma cons_wf filter-map filter_wf5 l_member_wf bnot_wf deq_wf
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 equalitySymmetry setElimination setEquality hyp_replacement Error :applyLambdaEquality,  natural_numberEquality imageMemberEquality baseClosed axiomEquality functionEquality universeEquality

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: 2016_10_21-AM-10_39_56
Last ObjectModification: 2016_07_12-AM-05_50_00

Theory : decidable!equality

Home Index