---

Step * 1 2 2 1 2 1 of Lemma polynom-equal-iff

.....assertion..... 
1. n : ℤ
2. 0 < n
3. ∀p,q:polynom(n - 1).
     ((↑poly-zero(n - 1;add-polynom(n - 1;tt;p;minus-polynom(n - 1;q)))) ⇒ (p = q ∈ polynom(n - 1)))
4. p : polynom(n - 1) List
5. q : polynom(n - 1) List
6. ↑poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
7. p ∈ polynom(n)
8. q ∈ polynom(n)
9. 0 < ||p|| ⇒ (¬↑poly-zero(n - 1;hd(p)))
10. 0 < ||q|| ⇒ (¬↑poly-zero(n - 1;hd(q)))
11. ∀q:polynom(n). (||minus-polynom(n;q)|| = ||q|| ∈ ℤ)
⊢ ||p|| = ||q|| ∈ ℤ
BY
{ (DupHyp (-6)
   THEN RecUnfold `add-polynom` (-1)
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN PromoteHyp (-1) 2
   THEN Reduce -1
   THEN RepeatFor 2 ((CallByValueReduce (-1)⋅ THENA Auto))) }

1
1. n : ℤ
2. ¬(n = 0 ∈ ℤ)
3. 0 < n
4. ∀p,q:polynom(n - 1).
     ((↑poly-zero(n - 1;add-polynom(n - 1;tt;p;minus-polynom(n - 1;q)))) ⇒ (p = q ∈ polynom(n - 1)))
5. p : polynom(n - 1) List
6. q : polynom(n - 1) List
7. ↑poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
8. p ∈ polynom(n)
9. q ∈ polynom(n)
10. 0 < ||p|| ⇒ (¬↑poly-zero(n - 1;hd(p)))
11. 0 < ||q|| ⇒ (¬↑poly-zero(n - 1;hd(q)))
12. ∀q:polynom(n). (||minus-polynom(n;q)|| = ||q|| ∈ ℤ)
13. ↑poly-zero(n;if null(p) then minus-polynom(n;q)
if null(minus-polynom(n;q)) then p
else eval m = ||p|| in
     eval k = ||minus-polynom(n;q)|| in
       if (m) < (k)
          then let b,bs = minus-polynom(n;q) 
               in let cs ⟵ add-polynom(n;ff;p;bs)
                  in [b / cs]
          else if (k) < (m)
                  then let a,as = p 
                       in let cs ⟵ add-polynom(n;ff;as;minus-polynom(n;q))
                          in [a / cs]
                  else let a,as = p 
                       in let b,bs = minus-polynom(n;q) 
                          in let c ⟵ add-polynom(n - 1;tt;a;b)
                             in let cs ⟵ add-polynom(n;ff;as;bs)
                                in rm-zeros(n - 1;[c / cs])
fi )
⊢ ||p|| = ||q|| ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}p,q:polynom(n  -  1).
          ((\muparrow{}poly-zero(n  -  1;add-polynom(n  -  1;tt;p;minus-polynom(n  -  1;q))))  {}\mRightarrow{}  (p  =  q))
4.  p  :  polynom(n  -  1)  List
5.  q  :  polynom(n  -  1)  List
6.  \muparrow{}poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
7.  p  \mmember{}  polynom(n)
8.  q  \mmember{}  polynom(n)
9.  0  <  ||p||  {}\mRightarrow{}  (\mneg{}\muparrow{}poly-zero(n  -  1;hd(p)))
10.  0  <  ||q||  {}\mRightarrow{}  (\mneg{}\muparrow{}poly-zero(n  -  1;hd(q)))
11.  \mforall{}q:polynom(n).  (||minus-polynom(n;q)||  =  ||q||)
\mvdash{}  ||p||  =  ||q||


By

---

Latex:
(DupHyp  (-6)
  THEN  RecUnfold  `add-polynom`  (-1)
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  PromoteHyp  (-1)  2
  THEN  Reduce  -1
  THEN  RepeatFor  2  ((CallByValueReduce  (-1)\mcdot{}  THENA  Auto)))

---

Home Index