---

Step * 2 2 1 1 1 of Lemma adjacent-to-last


1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. 0 < ||[u1 / v]|| + 1
6. no_repeats(T;[u; [u1 / v]])
7. a : T
8. 0 < ||[u1 / v]||
9. ((last([u1 / v]) = u ∈ T) ∧ (a = hd([u1 / v]) ∈ T)) ∨ adjacent(T;[u1 / v];last([u1 / v]);a)
10. ∀a:T. (adjacent(T;[u1 / v];last([u1 / v]);a) ⇐⇒ False) supposing no_repeats(T;[u1 / v])
⊢ False
BY
{ D (-2) }

1
1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. 0 < ||[u1 / v]|| + 1
6. no_repeats(T;[u; [u1 / v]])
7. a : T
8. 0 < ||[u1 / v]||
9. (last([u1 / v]) = u ∈ T) ∧ (a = hd([u1 / v]) ∈ T)
10. ∀a:T. (adjacent(T;[u1 / v];last([u1 / v]);a) ⇐⇒ False) supposing no_repeats(T;[u1 / v])
⊢ False

2
1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. 0 < ||[u1 / v]|| + 1
6. no_repeats(T;[u; [u1 / v]])
7. a : T
8. 0 < ||[u1 / v]||
9. adjacent(T;[u1 / v];last([u1 / v]);a)
10. ∀a:T. (adjacent(T;[u1 / v];last([u1 / v]);a) ⇐⇒ False) supposing no_repeats(T;[u1 / v])
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  u1  :  T
4.  v  :  T  List
5.  0  <  ||[u1  /  v]||  +  1
6.  no\_repeats(T;[u;  [u1  /  v]])
7.  a  :  T
8.  0  <  ||[u1  /  v]||
9.  ((last([u1  /  v])  =  u)  \mwedge{}  (a  =  hd([u1  /  v])))  \mvee{}  adjacent(T;[u1  /  v];last([u1  /  v]);a)
10.  \mforall{}a:T.  (adjacent(T;[u1  /  v];last([u1  /  v]);a)  \mLeftarrow{}{}\mRightarrow{}  False)  supposing  no\_repeats(T;[u1  /  v])
\mvdash{}  False


By

---

Latex:
D  (-2)

---

Home Index