---

Step * 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
⊢ ||let cs ⟵ add-polynom(n + 1;ff;[u / v];v1) in [u1 / cs]|| = imax(||v|| + 1;||v1|| + 1) ∈ ℤ
BY
{ ((Assert add-polynom(n + 1;ff;[u / v];v1) ∈ polyform(n + 1) BY
          (BLemma `add-polynom_wf1` THEN Auto THEN RecUnfold `polyform` 0 THEN Auto))
   THEN ((CallByValueReduce 0 THENM Reduce 0) THENA Auto)
   ) }

1
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)
⊢ (||add-polynom(n + 1;ff;[u / v];v1)|| + 1) = imax(||v|| + 1;||v1|| + 1) ∈ ℤ

---

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
\mvdash{}  ||let  cs  \mleftarrow{}{}  add-polynom(n  +  1;ff;[u  /  v];v1)  in  [u1  /  cs]||  =  imax(||v||  +  1;||v1||  +  1)


By

---

Latex:
((Assert  add-polynom(n  +  1;ff;[u  /  v];v1)  \mmember{}  polyform(n  +  1)  BY
                (BLemma  `add-polynom\_wf1`  THEN  Auto  THEN  RecUnfold  `polyform`  0  THEN  Auto))
  THEN  ((CallByValueReduce  0  THENM  Reduce  0)  THENA  Auto)
  )

---

Home Index