Step
*
2
2
of Lemma
sorted-by-unique
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
5. u : T
6. v : T List
7. ∀[sb:T List]
(v = sb ∈ (T List)) supposing
(no_repeats(T;v) and
sorted-by(R;v) and
no_repeats(T;sb) and
sorted-by(R;sb) and
set-equal(T;v;sb))
8. u1 : T
9. v1 : T List
10. ([u / v] = v1 ∈ (T List)) supposing
(no_repeats(T;[u / v]) and
sorted-by(R;[u / v]) and
no_repeats(T;v1) and
sorted-by(R;v1) and
set-equal(T;[u / v];v1))
⊢ ([u / v] = [u1 / v1] ∈ (T List)) supposing
(no_repeats(T;[u / v]) and
sorted-by(R;[u / v]) and
no_repeats(T;[u1 / v1]) and
sorted-by(R;[u1 / v1]) and
set-equal(T;[u / v];[u1 / v1]))
BY
{ (Thin (-1)
THEN Auto
THEN (AllHyps (RWO "no_repeats_cons") THENA Auto)
THEN (AllHyps (RWO "sorted-by-cons") THENA Auto)) }
1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
5. u : T
6. v : T List
7. ∀[sb:T List]
(v = sb ∈ (T List)) supposing
(no_repeats(T;v) and
sorted-by(R;v) and
no_repeats(T;sb) and
sorted-by(R;sb) and
set-equal(T;v;sb))
8. u1 : T
9. v1 : T List
10. set-equal(T;[u / v];[u1 / v1])
11. sorted-by(R;v1) ∧ (∀z∈v1.R u1 z)
12. no_repeats(T;v1) ∧ (¬(u1 ∈ v1))
13. sorted-by(R;v) ∧ (∀z∈v.R u z)
14. no_repeats(T;v) ∧ (¬(u ∈ v))
⊢ [u / v] = [u1 / v1] ∈ (T List)
Latex:
Latex:
1. T : Type
2. R : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
5. u : T
6. v : T List
7. \mforall{}[sb:T List]
(v = sb) supposing
(no\_repeats(T;v) and
sorted-by(R;v) and
no\_repeats(T;sb) and
sorted-by(R;sb) and
set-equal(T;v;sb))
8. u1 : T
9. v1 : T List
10. ([u / v] = v1) supposing
(no\_repeats(T;[u / v]) and
sorted-by(R;[u / v]) and
no\_repeats(T;v1) and
sorted-by(R;v1) and
set-equal(T;[u / v];v1))
\mvdash{} ([u / v] = [u1 / v1]) supposing
(no\_repeats(T;[u / v]) and
sorted-by(R;[u / v]) and
no\_repeats(T;[u1 / v1]) and
sorted-by(R;[u1 / v1]) and
set-equal(T;[u / v];[u1 / v1]))
By
Latex:
(Thin (-1)
THEN Auto
THEN (AllHyps (RWO "no\_repeats\_cons") THENA Auto)
THEN (AllHyps (RWO "sorted-by-cons") THENA Auto))
Home
Index