---

Step * of Lemma polyform-subtype

∀[n,m:ℕ].  polyform(n) ⊆r polyform(m) supposing n ≤ m
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN MoveToConcl (-1)
   THEN RepeatFor 3 (MoveToConcl (-2))
   THEN MoveToConcl (-1)) }

1
∀x:tree(ℤ). ∀n,m:ℕ.  ((n ≤ m) ⇒ (↑(ispolyform(x) n)) ⇒ (↑(ispolyform(x) m)))

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    polyform(n)  \msubseteq{}r  polyform(m)  supposing  n  \mleq{}  m


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  RepeatFor  3  (MoveToConcl  (-2))
  THEN  MoveToConcl  (-1))

---

Home Index