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

[T:Type]
∀eq:EqDecider(T). ∀L:T List. ∀x:T.
(((x ∈ L) ∧ (||remove-repeats(eq;L [x])|| ||remove-repeats(eq;L)|| ∈ ℤ))
∨ ((¬(x ∈ L)) ∧ (||remove-repeats(eq;L [x])|| (||remove-repeats(eq;L)|| 1) ∈ ℤ)))

Proof

Definitions occuring in Statement :  remove-repeats: remove-repeats(eq;L) l_member: (x ∈ l) length: ||as|| append: as bs cons: [a b] nil: [] list: List deq: EqDecider(T) uall: [x:A]. B[x] all: x:A. B[x] not: ¬A or: P ∨ Q and: P ∧ Q add: m natural_number: \$n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T implies:  Q decidable: Dec(P) or: P ∨ Q prop: and: P ∧ Q guard: {T} uimplies: supposing a set-equal: set-equal(T;x;y) iff: ⇐⇒ Q rev_implies:  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 list_wf deq_wf not_wf l_member_wf equal_wf length_wf remove-repeats_wf append_wf cons_wf nil_wf remove-repeats-set-equal member_append member_singleton or_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 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 universeEquality unionElimination inlFormation productEquality intEquality addEquality natural_numberEquality sqequalRule inrFormation independent_pairFormation independent_isectElimination addLevel productElimination 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.
(((x  \mmember{}  L)  \mwedge{}  (||remove-repeats(eq;L  @  [x])||  =  ||remove-repeats(eq;L)||))
\mvee{}  ((\mneg{}(x  \mmember{}  L))  \mwedge{}  (||remove-repeats(eq;L  @  [x])||  =  (||remove-repeats(eq;L)||  +  1))))

Date html generated: 2017_04_17-AM-09_10_32
Last ObjectModification: 2017_02_27-PM-05_19_03

Theory : decidable!equality

Home Index