---

Step * of Lemma compose-polynom_wf

∀[n:ℕ]. ∀[p,q:polynom(n)].  (compose-polynom(n;p;q) ∈ polynom(n))
BY
{ (ProveWfLemma THEN (Assert ⌜q ∈ polynom(n - 1) List⌝⋅ THENM Auto)) }

1
.....assertion..... 
1. n : ℕ
2. p : polynom(n)
3. q : polynom(n)
4. ¬(n = 0 ∈ ℤ)
⊢ q ∈ polynom(n - 1) List

2
1. n : ℕ
2. p : polynom(n)
3. q : polynom(n)
4. ¬(n = 0 ∈ ℤ)
5. q ∈ polynom(n - 1) List
6. z : polynom(n)
7. a : polynom(n - 1)
8. ¬↑poly-zero(n - 1;a)
⊢ [a] ∈ polynom(n)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p,q:polynom(n)].    (compose-polynom(n;p;q)  \mmember{}  polynom(n))


By

---

Latex:
(ProveWfLemma  THEN  (Assert  \mkleeneopen{}q  \mmember{}  polynom(n  -  1)  List\mkleeneclose{}\mcdot{}  THENM  Auto))

---

Home Index