### Nuprl Lemma : remove-repeats-append-one

`∀[T:Type]`
`  ∀eq:EqDecider(T). ∀L:T List. ∀x:T.`
`    ((||remove-repeats(eq;L @ [x])|| = ||remove-repeats(eq;L)|| ∈ ℤ)`
`    ∨ (||remove-repeats(eq;L @ [x])|| = (||remove-repeats(eq;L)|| + 1) ∈ ℤ))`

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` length: `||as||` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` or: `P ∨ Q` add: `n + m` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` implies: `P `` Q` decidable: `Dec(P)` or: `P ∨ Q` prop: `ℙ` guard: `{T}` uimplies: `b supposing a` set-equal: `set-equal(T;x;y)` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` sq_type: `SQType(T)` remove-repeats: `remove-repeats(eq;L)` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` squash: `↓T` true: `True` deq: `EqDecider(T)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` not: `¬A` uiff: `uiff(P;Q)` eqof: `eqof(d)` false: `False`
Lemmas referenced :  decidable__l_member decidable-equal-deq deq_wf equal_wf length_wf remove-repeats_wf append_wf cons_wf nil_wf remove-repeats-set-equal member_append member_singleton or_wf l_member_wf iff_wf and_wf set-equal-permute subtype_base_sq int_subtype_base list_ind_cons_lemma list_ind_nil_lemma length_of_cons_lemma filter_trivial2 bnot_wf l_all_iff assert_wf iff_transitivity eqof_wf not_wf iff_weakening_uiff assert_of_bnot safe-assert-deq member-remove-repeats
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache dependent_functionElimination hypothesisEquality independent_functionElimination hypothesis cumulativity unionElimination inlFormation intEquality addEquality natural_numberEquality sqequalRule inrFormation independent_isectElimination addLevel productElimination independent_pairFormation orFunctionality impliesFunctionality hyp_replacement equalitySymmetry dependent_set_memberEquality applyLambdaEquality setElimination rename instantiate equalityTransitivity isect_memberEquality voidElimination voidEquality applyEquality lambdaEquality imageElimination imageMemberEquality baseClosed setEquality

Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x:T.
((||remove-repeats(eq;L  @  [x])||  =  ||remove-repeats(eq;L)||)
\mvee{}  (||remove-repeats(eq;L  @  [x])||  =  (||remove-repeats(eq;L)||  +  1)))

Date html generated: 2017_04_17-AM-09_10_26
Last ObjectModification: 2017_02_27-PM-05_18_22

Theory : decidable!equality

Home Index