---

Step * 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||) ∈ ℤ
⊢ ||if (||v|| + 1) < (||v1|| + 1)
       then let cs ⟵ add-polynom(n + 1;ff;[u / v];v1)
            in [u1 / cs]
       else if (||v1|| + 1) < (||v|| + 1)
               then let cs ⟵ add-polynom(n + 1;ff;v;[u1 / v1])
                    in [u / cs]
               else let c ⟵ add-polynom((n + 1) - 1;tt;u;u1)
                    in let cs ⟵ add-polynom(n + 1;ff;v;v1)
                       in [c / cs]||
= imax(||v|| + 1;||v1|| + 1)
∈ ℤ
BY
{ ((Decide ⌜||v|| + 1 < ||v1|| + 1⌝⋅ 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
⊢ ||let cs ⟵ add-polynom(n + 1;ff;[u / v];v1) in [u1 / cs]|| = imax(||v|| + 1;||v1|| + 1) ∈ ℤ

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


By

---

Latex:
((Decide  \mkleeneopen{}||v||  +  1  <  ||v1||  +  1\mkleeneclose{}\mcdot{}  THENM  Reduce  0)  THENA  Auto)

---

Home Index