---

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


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|| ∈ ℤ
BY
{ ((Assert polynom(n) ⊆r (polynom(n - 1) List) BY
          Auto)
   THEN (Assert minus-polynom(n;q) ∈ polynom(n - 1) List BY
               (SubsumeC ⌜polynom(n)⌝⋅ THEN 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 )
14. polynom(n) ⊆r (polynom(n - 1) List)
15. minus-polynom(n;q) ∈ polynom(n - 1) List
⊢ ||p|| = ||q|| ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  \mneg{}(n  =  0)
3.  0  <  n
4.  \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))
5.  p  :  polynom(n  -  1)  List
6.  q  :  polynom(n  -  1)  List
7.  \muparrow{}poly-zero(n;add-polynom(n;tt;p;minus-polynom(n;q)))
8.  p  \mmember{}  polynom(n)
9.  q  \mmember{}  polynom(n)
10.  0  <  ||p||  {}\mRightarrow{}  (\mneg{}\muparrow{}poly-zero(n  -  1;hd(p)))
11.  0  <  ||q||  {}\mRightarrow{}  (\mneg{}\muparrow{}poly-zero(n  -  1;hd(q)))
12.  \mforall{}q:polynom(n).  (||minus-polynom(n;q)||  =  ||q||)
13.  \muparrow{}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  \mleftarrow{}{}  add-polynom(n;ff;p;bs)
                                    in  [b  /  cs]
                    else  if  (k)  <  (m)
                                    then  let  a,as  =  p 
                                              in  let  cs  \mleftarrow{}{}  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  \mleftarrow{}{}  add-polynom(n  -  1;tt;a;b)
                                                          in  let  cs  \mleftarrow{}{}  add-polynom(n;ff;as;bs)
                                                                in  rm-zeros(n  -  1;[c  /  cs])
fi  )
\mvdash{}  ||p||  =  ||q||


By

---

Latex:
((Assert  polynom(n)  \msubseteq{}r  (polynom(n  -  1)  List)  BY
                Auto)
  THEN  (Assert  minus-polynom(n;q)  \mmember{}  polynom(n  -  1)  List  BY
                          (SubsumeC  \mkleeneopen{}polynom(n)\mkleeneclose{}\mcdot{}  THEN  Auto))
  )

---

Home Index