---

Step * of Lemma add-ipoly-ringeq

No Annotations
∀r:Rng. ∀p,q:iMonomial() List.  ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)
BY
{ (Auto
   THEN (Assert ⌜∀n:ℕ. ∀p,q:iMonomial() List.
                   (||p|| + ||q|| < n
                   ⇒ ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q))⌝⋅
   THENM ((InstHyp [⌜(||p|| + ||q||) + 1⌝] (-1)⋅ THENM BHyp -1) THEN Auto)
   )
   THEN All Thin
   THEN InductionOnNat
   THEN Auto) }

1
1. r : Rng
2. n : ℤ
3. p : iMonomial() List
4. q : iMonomial() List
5. ||p|| + ||q|| < 0
⊢ ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)

2
1. r : Rng
2. n : ℤ
3. 0 < n
4. ∀p,q:iMonomial() List.
     (||p|| + ||q|| < n - 1 ⇒ ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q))
5. p : iMonomial() List
6. q : iMonomial() List
7. ||p|| + ||q|| < n
⊢ ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)

---

Latex:

---

Latex:
No  Annotations
\mforall{}r:Rng.  \mforall{}p,q:iMonomial()  List.
    ipolynomial-term(add-ipoly(p;q))  \mequiv{}  ipolynomial-term(p)  (+)  ipolynomial-term(q)


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}p,q:iMonomial()  List.
                                  (||p||  +  ||q||  <  n
                                  {}\mRightarrow{}  ipolynomial-term(add-ipoly(p;q))  \mequiv{}  ipolynomial-term(p)  (+)  ipolynomial-term(q))\mkleeneclose{}
              \mcdot{}
  THENM  ((InstHyp  [\mkleeneopen{}(||p||  +  ||q||)  +  1\mkleeneclose{}]  (-1)\mcdot{}  THENM  BHyp  -1)  THEN  Auto)
  )
  THEN  All  Thin
  THEN  InductionOnNat
  THEN  Auto)

---

Home Index