---

Step * 4 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);minus-poly(int_term_to_ipoly(right)))) ≡ left (-) right
BY
{ xxx(((InstLemma `add-ipoly-ringeq` [⌜r⌝]⋅ THENA Auto) THEN (InstLemma `minus-poly-ringeq` [⌜r⌝]⋅ THENA Auto))
      THEN RWW "add_ipoly-sq -1 -2 -3 -4" 0
      THEN Auto
      THEN D 0
      THEN Reduce 0
      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);minus-poly(int\_term\_to\_ipoly(right))))  \mequiv{}  left 
(-)  right


By

---

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

---

Home Index