---

Step * 1 of Lemma poly-zero-val


1. p : tree(ℤ)
2. ↑poly-zero(p)
3. l : Top
⊢ p@l = 0 ∈ ℤ
BY
{ (D 1 THEN RepUR ``poly-zero`` -2 THEN Auto) }

1
1. p1 : ℤ
2. ↑(p1 =z 0)
3. l : Top
⊢ tree_leaf(p1)@l = 0 ∈ ℤ

---

Latex:

---

Latex:

1.  p  :  tree(\mBbbZ{})
2.  \muparrow{}poly-zero(p)
3.  l  :  Top
\mvdash{}  p@l  =  0


By

---

Latex:
(D  1  THEN  RepUR  ``poly-zero``  -2  THEN  Auto)

---

Home Index