---

Step * 3 of Lemma ring_term_polynomial


1. r : CRng
2. left : int_term()
3. right : int_term()
4. ipolynomial-term(int_term_to_ipoly(left)) ≡ left
5. ipolynomial-term(int_term_to_ipoly(right)) ≡ right
⊢ ipolynomial-term(add_ipoly(int_term_to_ipoly(left);int_term_to_ipoly(right))) ≡ left (+) right
BY
{ xxx((InstLemma `add-ipoly-ringeq` [⌜r⌝]⋅ THENA Auto)
      THEN RWW "add_ipoly-sq -1 -2 -3" 0
      THEN Auto
      THEN RelRST
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  left  :  int\_term()
3.  right  :  int\_term()
4.  ipolynomial-term(int\_term\_to\_ipoly(left))  \mequiv{}  left
5.  ipolynomial-term(int\_term\_to\_ipoly(right))  \mequiv{}  right
\mvdash{}  ipolynomial-term(add\_ipoly(int\_term\_to\_ipoly(left);int\_term\_to\_ipoly(right)))  \mequiv{}  left  (+)  right


By

---

Latex:
xxx((InstLemma  `add-ipoly-ringeq`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  RWW  "add\_ipoly-sq  -1  -2  -3"  0
        THEN  Auto
        THEN  RelRST
        THEN  Auto)xxx

---

Home Index