---

Step * of Lemma ispolyform_node_lemma

∀n,b,a:Top.  (ispolyform(tree_node(a;b)) n ~ ((ispolyform(a) (n - 1)) ∧b (ispolyform(b) n)) ∧b 0 <z n)
BY
{ (RepUR ``ispolyform`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n,b,a:Top.
    (ispolyform(tree\_node(a;b))  n  \msim{}  ((ispolyform(a)  (n  -  1))  \mwedge{}\msubb{}  (ispolyform(b)  n))  \mwedge{}\msubb{}  0  <z  n)


By

---

Latex:
(RepUR  ``ispolyform``  0  THEN  Auto)

---

Home Index