### Nuprl Lemma : remove_repeats_cons_lemma

`∀v,u,eq:Top.  (remove-repeats(eq;[u / v]) ~ [u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])`

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` filter: `filter(P;l)` cons: `[a / b]` bnot: `¬bb` top: `Top` all: `∀x:A. B[x]` apply: `f a` lambda: `λx.A[x]` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` remove-repeats: `remove-repeats(eq;L)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  top_wf list_ind_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}v,u,eq:Top.    (remove-repeats(eq;[u  /  v])  \msim{}  [u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v))])

Date html generated: 2016_05_14-PM-03_26_34
Last ObjectModification: 2015_12_26-PM-06_23_07

Theory : decidable!equality

Home Index