---

Step * 2 of Lemma polyvar_wf


1. v : ℤ
2. v ≠ 0
3. 0 < v
4. polyvar(v - 1) ∈ {p:polynom((v - 1) + 1)| poly-zero(p) = ff ∧ poly-int(p) = ff} 
5. v1 : polynom(v)
6. poly-zero(v1) = ff
7. poly-int(v1) = ff
8. poly-zero(tree_node(v1;tree_leaf(0))) = ff
⊢ poly-int(tree_node(v1;tree_leaf(0))) = ff
BY
{ (RepUR ``poly-int`` 0 THEN Fold `poly-int` 0 THEN RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}
2.  v  \mneq{}  0
3.  0  <  v
4.  polyvar(v  -  1)  \mmember{}  \{p:polynom((v  -  1)  +  1)|  poly-zero(p)  =  ff  \mwedge{}  poly-int(p)  =  ff\} 
5.  v1  :  polynom(v)
6.  poly-zero(v1)  =  ff
7.  poly-int(v1)  =  ff
8.  poly-zero(tree\_node(v1;tree\_leaf(0)))  =  ff
\mvdash{}  poly-int(tree\_node(v1;tree\_leaf(0)))  =  ff


By

---

Latex:
(RepUR  ``poly-int``  0  THEN  Fold  `poly-int`  0  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index