---

Step * 2 of Lemma adjacent-to-last


1. [T] : Type
2. u : T
3. v : T List
4. (∀a:T. (adjacent(T;v;last(v);a) ⇐⇒ False)) supposing (no_repeats(T;v) and 0 < ||v||)
⊢ (∀a:T. (adjacent(T;[u / v];last([u / v]);a) ⇐⇒ False)) supposing (no_repeats(T;[u / v]) and 0 < ||v|| + 1)
BY
{ DVar `v' }

1
1. [T] : Type
2. u : T
3. (∀a:T. (adjacent(T;[];last([]);a) ⇐⇒ False)) supposing (no_repeats(T;[]) and 0 < ||[]||)
⊢ (∀a:T. (adjacent(T;[u];last([u]);a) ⇐⇒ False)) supposing (no_repeats(T;[u]) and 0 < ||[]|| + 1)

2
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]||)
⊢ (∀a:T. (adjacent(T;[u; [u1 / v]];last([u; [u1 / v]]);a) ⇐⇒ False)) supposing 
     (no_repeats(T;[u; [u1 / v]]) and 
     0 < ||[u1 / v]|| + 1)

---

Latex:

---

Latex:

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


By

---

Latex:
DVar  `v'

---

Home Index