---

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


1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. (∀a:T. (adjacent(T;[u1 / v];last([u1 / v]);a) ⇐⇒ False)) supposing (no_repeats(T;[u1 / v]) and 0 < ||[u1 / v]||)
6. 0 < ||[u1 / v]|| + 1
7. no_repeats(T;[u; [u1 / v]])
8. a : T
9. adjacent(T;[u; [u1 / v]];last([u; [u1 / v]]);a)
⊢ False
BY
{ (RWO "last_cons" (-1) THENA (Auto THEN Reduce 0 THEN Auto))⋅ }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "last\_cons"  (-1)  THENA  (Auto  THEN  Reduce  0  THEN  Auto))\mcdot{}

---

Home Index