---

Step * of Lemma add-poly-prepend-sq1

∀[p,q,l:(ℤ × (ℤ List)) List].  (add-ipoly-prepend(p;q;l) ~ rev(l) + add-ipoly(p;q))
BY
{ InductionOnList }

1
∀[q,l:(ℤ × (ℤ List)) List].  (add-ipoly-prepend([];q;l) ~ rev(l) + add-ipoly([];q))

2
1. u : ℤ × (ℤ List)
2. v : (ℤ × (ℤ List)) List
3. ∀[q,l:(ℤ × (ℤ List)) List].  (add-ipoly-prepend(v;q;l) ~ rev(l) + add-ipoly(v;q))
⊢ ∀[q,l:(ℤ × (ℤ List)) List].  (add-ipoly-prepend([u / v];q;l) ~ rev(l) + add-ipoly([u / v];q))

---

Latex:

---

Latex:
\mforall{}[p,q,l:(\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List].    (add-ipoly-prepend(p;q;l)  \msim{}  rev(l)  +  add-ipoly(p;q))


By

---

Latex:
InductionOnList

---

Home Index