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