---

Step * 1 1 1 1 of Lemma length2-decomp


1. [T] : Type
2. L : T List
3. ||L|| ≥ 2 
4. L ~ firstn(||L|| - 2;L) @ nth_tl(||L|| - 2;L)
5. v : T List
6. nth_tl(||L|| - 2;L) = v ∈ (T List)
⊢ (||v|| = 2 ∈ ℤ) ⇒ (∃a,b:T. (v = [a; b] ∈ (T List)))
BY
{ RepeatFor 3 ((D (-2) THEN Reduce 0 THEN Try (Complete (Auto')))) }

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  3  ((D  (-2)  THEN  Reduce  0  THEN  Try  (Complete  (Auto'))))

---

Home Index