---

Step * 2 1 1 2 2 1 of Lemma add-polynom-int-val


1. n : {1...}
2. u : ℤ
3. v : ℤ List
4. ∀[p,q:polyform(n - 1)]. ∀[rmz:𝔹].  (add-polynom(n - 1;rmz;p;q)@v = (p@v + q@v) ∈ ℤ)
5. v ∈ {l:ℤ List| ||l|| = (n - 1) ∈ ℤ} 
6. [u / v] ∈ {l:ℤ List| ||l|| = n ∈ ℤ} 
7. u1 : polyform(n - 1)
8. v1 : polyform(n - 1) List
9. ∀[q:polyform(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;v1;q)@[u / v] = (v1@[u / v] + q@[u / v]) ∈ ℤ)
10. u2 : polyform(n - 1)
11. v2 : polyform(n - 1) List
12. ∀[rmz:𝔹]. (add-polynom(n;rmz;[u1 / v1];v2)@[u / v] = ([u1 / v1]@[u / v] + v2@[u / v]) ∈ ℤ)
13. [u1 / v1] ∈ polyform(n)
14. v1 ∈ polyform(n)
15. [u2 / v2] ∈ polyform(n)
16. v2 ∈ polyform(n)
17. rmz : 𝔹
⊢ add-polynom(n;rmz;[u1 / v1];[u2 / v2])@[u / v]
= (((u1@v * u^||v1||) + v1@[u / v]) + (u2@v * u^||v2||) + v2@[u / v])
∈ ℤ
BY
{ (RecUnfold `add-polynom` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. n : {1...}
2. u : ℤ
3. v : ℤ List
4. ∀[p,q:polyform(n - 1)]. ∀[rmz:𝔹].  (add-polynom(n - 1;rmz;p;q)@v = (p@v + q@v) ∈ ℤ)
5. v ∈ {l:ℤ List| ||l|| = (n - 1) ∈ ℤ} 
6. [u / v] ∈ {l:ℤ List| ||l|| = n ∈ ℤ} 
7. u1 : polyform(n - 1)
8. v1 : polyform(n - 1) List
9. ∀[q:polyform(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;v1;q)@[u / v] = (v1@[u / v] + q@[u / v]) ∈ ℤ)
10. u2 : polyform(n - 1)
11. v2 : polyform(n - 1) List
12. ∀[rmz:𝔹]. (add-polynom(n;rmz;[u1 / v1];v2)@[u / v] = ([u1 / v1]@[u / v] + v2@[u / v]) ∈ ℤ)
13. [u1 / v1] ∈ polyform(n)
14. v1 ∈ polyform(n)
15. [u2 / v2] ∈ polyform(n)
16. v2 ∈ polyform(n)
17. rmz : 𝔹
18. ¬(n = 0 ∈ ℤ)
⊢ if (||v1|| + 1) < (||v2|| + 1)
     then let cs ⟵ add-polynom(n;ff;[u1 / v1];v2)
          in [u2 / cs]
     else if (||v2|| + 1) < (||v1|| + 1)
             then let cs ⟵ add-polynom(n;ff;v1;[u2 / v2])
                  in [u1 / cs]
             else let c ⟵ add-polynom(n - 1;tt;u1;u2)
                  in let cs ⟵ add-polynom(n;ff;v1;v2)
                     in if rmz then rm-zeros(n - 1;[c / cs]) else [c / cs] fi @[u / v]
= (((u1@v * u^||v1||) + v1@[u / v]) + (u2@v * u^||v2||) + v2@[u / v])
∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  \mforall{}[p,q:polyform(n  -  1)].  \mforall{}[rmz:\mBbbB{}].    (add-polynom(n  -  1;rmz;p;q)@v  =  (p@v  +  q@v))
5.  v  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  (n  -  1)\} 
6.  [u  /  v]  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  n\} 
7.  u1  :  polyform(n  -  1)
8.  v1  :  polyform(n  -  1)  List
9.  \mforall{}[q:polyform(n  -  1)  List].  \mforall{}[rmz:\mBbbB{}].
          (add-polynom(n;rmz;v1;q)@[u  /  v]  =  (v1@[u  /  v]  +  q@[u  /  v]))
10.  u2  :  polyform(n  -  1)
11.  v2  :  polyform(n  -  1)  List
12.  \mforall{}[rmz:\mBbbB{}].  (add-polynom(n;rmz;[u1  /  v1];v2)@[u  /  v]  =  ([u1  /  v1]@[u  /  v]  +  v2@[u  /  v]))
13.  [u1  /  v1]  \mmember{}  polyform(n)
14.  v1  \mmember{}  polyform(n)
15.  [u2  /  v2]  \mmember{}  polyform(n)
16.  v2  \mmember{}  polyform(n)
17.  rmz  :  \mBbbB{}
\mvdash{}  add-polynom(n;rmz;[u1  /  v1];[u2  /  v2])@[u  /  v]
=  (((u1@v  *  u\^{}||v1||)  +  v1@[u  /  v])  +  (u2@v  *  u\^{}||v2||)  +  v2@[u  /  v])


By

---

Latex:
(RecUnfold  `add-polynom`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index