---

Step * 2 of Lemma length-minus-polynom

.....falsecase..... 
1. n : ℕ+
2. p : polyform(n - 1) List
3. ¬(n = 0 ∈ ℤ)
⊢ ||minus-polynom(n;p)|| = ||p|| ∈ ℤ
BY
{ (RecUnfold `minus-polynom` 0 THEN Reduce 0) }

1
1. n : ℕ+
2. p : polyform(n - 1) List
3. ¬(n = 0 ∈ ℤ)
⊢ ||map-rev(λq.minus-polynom(n - 1;q);p)|| = ||p|| ∈ ℤ

---

Latex:

---

Latex:
.....falsecase..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  p  :  polyform(n  -  1)  List
3.  \mneg{}(n  =  0)
\mvdash{}  ||minus-polynom(n;p)||  =  ||p||


By

---

Latex:
(RecUnfold  `minus-polynom`  0  THEN  Reduce  0)

---

Home Index