---

Step * 2 2 1 1 1 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. ∀[i,j:ℕ].
     (¬([u; [u1 / v]][i] = [u; [u1 / v]][j] ∈ T)) supposing 
        ((¬(i = j ∈ ℕ)) and 
        j < ||[u; [u1 / v]]|| and 
        i < ||[u; [u1 / v]]||)
7. a : T
8. 0 < ||[u1 / v]||
9. last([u1 / v]) = u ∈ T
10. a = hd([u1 / v]) ∈ T
11. ∀a:T. (adjacent(T;[u1 / v];last([u1 / v]);a) ⇐⇒ False) supposing no_repeats(T;[u1 / v])
⊢ u = [u; [u1 / v]][((||v|| + 1) + 1) - 1] ∈ T
BY
{ (RWO "select_cons_tl" 0 THEN Auto') }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "select\_cons\_tl"  0  THEN  Auto')

---

Home Index