---

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


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. ∀q:polynom(n). (||minus-polynom(n;q)|| = ||q|| ∈ ℤ)
5. ∀p,q:polynom(n - 1) List. ∀rmz:𝔹.  (poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q))) ∈ 𝔹)
6. k : ℤ
7. 0 < k
8. ∀p,q:polynom(n - 1) List. ∀rmz:𝔹.
     ((||p|| ≤ (k - 1))
     ⇒ (||p|| = ||q|| ∈ ℤ)
     ⇒ (↑poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q))))
     ⇒ (p = q ∈ (polynom(n - 1) List)))
9. p : polynom(n - 1) List
10. q : polynom(n - 1) List
11. rmz : 𝔹
12. ||p|| ≤ k
13. ||p|| = ||q|| ∈ ℤ
14. ↑poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q)))
⊢ p = q ∈ (polynom(n - 1) List)
BY
{ (RecUnfold `add-polynom` (-1)
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN PromoteHyp (-1) 2
   THEN Reduce -1
   THEN (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. ∀q:polynom(n). (||minus-polynom(n;q)|| = ||q|| ∈ ℤ)
6. ∀p,q:polynom(n - 1) List. ∀rmz:𝔹.  (poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q))) ∈ 𝔹)
7. k : ℤ
8. 0 < k
9. ∀p,q:polynom(n - 1) List. ∀rmz:𝔹.
     ((||p|| ≤ (k - 1))
     ⇒ (||p|| = ||q|| ∈ ℤ)
     ⇒ (↑poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q))))
     ⇒ (p = q ∈ (polynom(n - 1) List)))
10. p : polynom(n - 1) List
11. q : polynom(n - 1) List
12. rmz : 𝔹
13. ||p|| ≤ k
14. ||p|| = ||q|| ∈ ℤ
15. ↑poly-zero(n;let qq ⟵ minus-polynom(n;q)
                 in if null(p) then qq
                 if null(qq) then p
                 else eval m = ||p|| in
                      eval k = ||qq|| in
                        if (m) < (k)
                           then let b,bs = qq 
                                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;qq)
                                           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 if rmz then rm-zeros(n - 1;[c / cs]) else [c / cs] fi 
                 fi )
⊢ p = q ∈ (polynom(n - 1) List)

---

Latex:

---

Latex:

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.  \mforall{}q:polynom(n).  (||minus-polynom(n;q)||  =  ||q||)
5.  \mforall{}p,q:polynom(n  -  1)  List.  \mforall{}rmz:\mBbbB{}.    (poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q)))  \mmember{}  \mBbbB{})
6.  k  :  \mBbbZ{}
7.  0  <  k
8.  \mforall{}p,q:polynom(n  -  1)  List.  \mforall{}rmz:\mBbbB{}.
          ((||p||  \mleq{}  (k  -  1))
          {}\mRightarrow{}  (||p||  =  ||q||)
          {}\mRightarrow{}  (\muparrow{}poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q))))
          {}\mRightarrow{}  (p  =  q))
9.  p  :  polynom(n  -  1)  List
10.  q  :  polynom(n  -  1)  List
11.  rmz  :  \mBbbB{}
12.  ||p||  \mleq{}  k
13.  ||p||  =  ||q||
14.  \muparrow{}poly-zero(n;add-polynom(n;rmz;p;minus-polynom(n;q)))
\mvdash{}  p  =  q


By

---

Latex:
(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  (CallByValueReduce  (-1)\mcdot{}  THENA  Auto))

---

Home Index