---

Step * 1 of Lemma polyform-subtype


∀x:tree(ℤ). ∀n,m:ℕ.  ((n ≤ m) ⇒ (↑(ispolyform(x) n)) ⇒ (↑(ispolyform(x) m)))
BY
{ (BLemma `tree-induction` THEN Auto THEN All Reduce THEN All (RW assert_pushdownC) THEN Auto) }

1
1. left : tree(ℤ)
2. right : tree(ℤ)
3. ∀n,m:ℕ.  ((n ≤ m) ⇒ (↑(ispolyform(left) n)) ⇒ (↑(ispolyform(left) m)))
4. ∀n,m:ℕ.  ((n ≤ m) ⇒ (↑(ispolyform(right) n)) ⇒ (↑(ispolyform(right) m)))
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ↑(ispolyform(left) (n - 1))
9. ↑(ispolyform(right) n)
10. 0 < n
⊢ ↑(ispolyform(left) (m - 1))

---

Latex:

---

Latex:

\mforall{}x:tree(\mBbbZ{}).  \mforall{}n,m:\mBbbN{}.    ((n  \mleq{}  m)  {}\mRightarrow{}  (\muparrow{}(ispolyform(x)  n))  {}\mRightarrow{}  (\muparrow{}(ispolyform(x)  m)))


By

---

Latex:
(BLemma  `tree-induction`  THEN  Auto  THEN  All  Reduce  THEN  All  (RW  assert\_pushdownC)  THEN  Auto)

---

Home Index