---

Step * 1 of Lemma add-ipoly-equiv


1. p : iMonomial() List
2. q : iMonomial() List
⊢ ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)
BY
{ ((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. n : ℤ
2. p : iMonomial() List
3. q : iMonomial() List
4. ||p|| + ||q|| < 0
⊢ ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)

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

---

Latex:

---

Latex:

1.  p  :  iMonomial()  List
2.  q  :  iMonomial()  List
\mvdash{}  ipolynomial-term(add-ipoly(p;q))  \mequiv{}  ipolynomial-term(p)  (+)  ipolynomial-term(q)


By

---

Latex:
((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