---

Step * 1 2 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. ∃a,b:T. (nth_tl(||L|| - 2;L) = [a; b] ∈ (T List))
⊢ ∃a,b:T. ∃L':T List. (L = (L' @ [a; b]) ∈ (T List))
BY
{ (RepeatFor 2 (ParallelLast) THEN InstConcl [⌜firstn(||L|| - 2;L)⌝]⋅ THEN 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.  \mexists{}a,b:T.  (nth\_tl(||L||  -  2;L)  =  [a;  b])
\mvdash{}  \mexists{}a,b:T.  \mexists{}L':T  List.  (L  =  (L'  @  [a;  b]))


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  InstConcl  [\mkleeneopen{}firstn(||L||  -  2;L)\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index