---

Step * of Lemma poly-zero-implies

∀n:ℕ. ∀p:polyform(n).  ((↑poly-zero(n;p)) ⇒ (∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . (l@p = 0 ∈ ℤ)))
BY
{ (Auto
   THEN RecUnfold `polyform` 2
   THEN Unfold `poly-zero` -2
   THEN (SplitOnHypITE 2  THENA Auto)
   THEN SplitOnHypITE 3 
   THEN Auto
   THEN RepeatFor 2 (DVar `l')
   THEN All Reduce
   THEN Try (((Assert 0 ≤ ||v|| BY Auto) THEN Auto))
   THEN ((D -1 THEN Complete (Auto)) ORELSE (RecUnfold `poly-int-val` 0 THEN Reduce 0))) }

1
1. n : ℕ
2. p : ℤ
3. ↑(p =z 0)
4. 0 = n ∈ ℤ
5. n = 0 ∈ ℤ
6. n = 0 ∈ ℤ
⊢ p = 0 ∈ ℤ

2
1. n : ℕ
2. p : polyform(n - 1) List
3. ↑null(p)
4. u : ℤ
5. v : ℤ List
6. (||v|| + 1) = n ∈ ℤ
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
9. 0 ≤ ||v||
⊢ Σ(v@p[i] * u^||p|| - 1 - i | i < ||p||) = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}p:polyform(n).    ((\muparrow{}poly-zero(n;p))  {}\mRightarrow{}  (\mforall{}l:\{l:\mBbbZ{}  List|  ||l||  =  n\}  .  (l@p  =  0)))


By

---

Latex:
(Auto
  THEN  RecUnfold  `polyform`  2
  THEN  Unfold  `poly-zero`  -2
  THEN  (SplitOnHypITE  2    THENA  Auto)
  THEN  SplitOnHypITE  3 
  THEN  Auto
  THEN  RepeatFor  2  (DVar  `l')
  THEN  All  Reduce
  THEN  Try  (((Assert  0  \mleq{}  ||v||  BY  Auto)  THEN  Auto))
  THEN  ((D  -1  THEN  Complete  (Auto))  ORELSE  (RecUnfold  `poly-int-val`  0  THEN  Reduce  0)))

---

Home Index