---

Step * 2 1 of Lemma length-minus-polynom


1. n : ℕ+
2. p : polyform(n - 1) List
3. ¬(n = 0 ∈ ℤ)
⊢ ||map-rev(λq.minus-polynom(n - 1;q);p)|| = ||p|| ∈ ℤ
BY
{ ((InstLemma `map-rev-sq-map` [⌜polyform(n - 1)⌝;⌜polyform(n - 1)⌝]⋅ THENA Auto) THEN RWW "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `map-rev-sq-map`  [\mkleeneopen{}polyform(n  -  1)\mkleeneclose{};\mkleeneopen{}polyform(n  -  1)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWW  "-1"  0
  THEN  Auto)

---

Home Index