---

Step * 1 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
⊢ tree_node(v1;tree_leaf(0)) ∈ {p:polyform(v + 1)| (↑poly-int(p)) ⇒ (↑tree_leaf?(p))} 
BY
{ (MemTypeCD THEN Auto) }

1
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
⊢ tree_node(v1;tree_leaf(0)) ∈ polyform(v + 1)

2
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-int(tree_node(v1;tree_leaf(0)))
⊢ False

---

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
\mvdash{}  tree\_node(v1;tree\_leaf(0))  \mmember{}  \{p:polyform(v  +  1)|  (\muparrow{}poly-int(p))  {}\mRightarrow{}  (\muparrow{}tree\_leaf?(p))\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index