---

Step * 1 2 1 1 1 2 of Lemma last-lemma-sq


1. T : Type
2. L : T List
3. ¬↑null(L)
4. ||L|| > 0
5. nth_tl(||L|| - 1;L) ~ [hd(nth_tl(||L|| - 1;L)) / tl(nth_tl(||L|| - 1;L))]
⊢ [] ~ tl(nth_tl(||L|| - 1;L))
BY
{ Assert ||nth_tl(||L|| - 1;L)|| = 1 ∈ ℕ⋅ }

1
.....assertion..... 
1. T : Type
2. L : T List
3. ¬↑null(L)
4. ||L|| > 0
5. nth_tl(||L|| - 1;L) ~ [hd(nth_tl(||L|| - 1;L)) / tl(nth_tl(||L|| - 1;L))]
⊢ ||nth_tl(||L|| - 1;L)|| = 1 ∈ ℕ

2
1. T : Type
2. L : T List
3. ¬↑null(L)
4. ||L|| > 0
5. nth_tl(||L|| - 1;L) ~ [hd(nth_tl(||L|| - 1;L)) / tl(nth_tl(||L|| - 1;L))]
6. ||nth_tl(||L|| - 1;L)|| = 1 ∈ ℕ
⊢ [] ~ tl(nth_tl(||L|| - 1;L))

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  \mneg{}\muparrow{}null(L)
4.  ||L||  >  0
5.  nth\_tl(||L||  -  1;L)  \msim{}  [hd(nth\_tl(||L||  -  1;L))  /  tl(nth\_tl(||L||  -  1;L))]
\mvdash{}  []  \msim{}  tl(nth\_tl(||L||  -  1;L))


By

---

Latex:
Assert  ||nth\_tl(||L||  -  1;L)||  =  1\mcdot{}

---

Home Index