---

Step * 1 1 1 1 of Lemma add-polynom-length


1. n : ℕ
2. n + 1 ≠ 0
3. u : polyform(n)
4. v : polyform(n) List
5. ∀[q:polyform(n) List]. (||add-polynom(n + 1;ff;v;q)|| = imax(||v||;||q||) ∈ ℤ)
6. u1 : polyform(n)
7. v1 : polyform(n) List
8. ||add-polynom(n + 1;ff;[u / v];v1)|| = imax(||[u / v]||;||v1||) ∈ ℤ
9. ||v|| + 1 < ||v1|| + 1
10. add-polynom(n + 1;ff;[u / v];v1) ∈ polyform(n + 1)
⊢ (imax(||v|| + 1;||v1||) + 1) = imax(||v|| + 1;||v1|| + 1) ∈ ℤ
BY
{ (RWO "imax_unfold" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  n  +  1  \mneq{}  0
3.  u  :  polyform(n)
4.  v  :  polyform(n)  List
5.  \mforall{}[q:polyform(n)  List].  (||add-polynom(n  +  1;ff;v;q)||  =  imax(||v||;||q||))
6.  u1  :  polyform(n)
7.  v1  :  polyform(n)  List
8.  ||add-polynom(n  +  1;ff;[u  /  v];v1)||  =  imax(||[u  /  v]||;||v1||)
9.  ||v||  +  1  <  ||v1||  +  1
10.  add-polynom(n  +  1;ff;[u  /  v];v1)  \mmember{}  polyform(n  +  1)
\mvdash{}  (imax(||v||  +  1;||v1||)  +  1)  =  imax(||v||  +  1;||v1||  +  1)


By

---

Latex:
(RWO  "imax\_unfold"  0  THEN  Auto)

---

Home Index