---

Step * 1 1 of Lemma length2-decomp

.....assertion..... 
1. [T] : Type
2. L : T List
3. ||L|| ≥ 2 
4. L ~ firstn(||L|| - 2;L) @ nth_tl(||L|| - 2;L)
⊢ ∃a,b:T. (nth_tl(||L|| - 2;L) = [a; b] ∈ (T List))
BY
{ (Assert ||nth_tl(||L|| - 2;L)|| = 2 ∈ ℤ BY
         (RWO "length_nth_tl" 0 THEN Auto')) }

1
1. [T] : Type
2. L : T List
3. ||L|| ≥ 2 
4. L ~ firstn(||L|| - 2;L) @ nth_tl(||L|| - 2;L)
5. ||nth_tl(||L|| - 2;L)|| = 2 ∈ ℤ
⊢ ∃a,b:T. (nth_tl(||L|| - 2;L) = [a; b] ∈ (T List))

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  L  :  T  List
3.  ||L||  \mgeq{}  2 
4.  L  \msim{}  firstn(||L||  -  2;L)  @  nth\_tl(||L||  -  2;L)
\mvdash{}  \mexists{}a,b:T.  (nth\_tl(||L||  -  2;L)  =  [a;  b])


By

---

Latex:
(Assert  ||nth\_tl(||L||  -  2;L)||  =  2  BY
              (RWO  "length\_nth\_tl"  0  THEN  Auto'))

---

Home Index