---

Step * of Lemma ring_term_polynomial

∀r:CRng. ∀t:int_term().  ipolynomial-term(int_term_to_ipoly(t)) ≡ t
BY
{ xxx(Intro
      THEN BLemma `int_term-induction`
      THEN Auto
      THEN Unfold `int_term_to_ipoly` 0
      THEN Reduce 0
      THEN Try (Fold `int_term_to_ipoly` 0))xxx }

1
1. r : CRng
2. const : ℤ
⊢ ipolynomial-term(if const=0 then [] else [<const, []>]) ≡ "const"

2
1. r : CRng
2. var : ℤ
⊢ ipolynomial-term([<1, [var]>]) ≡ vvar

3
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

4
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

5
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(mul_ipoly(int_term_to_ipoly(left);int_term_to_ipoly(right))) ≡ left (*) right

6
1. r : CRng
2. num : int_term()
3. ipolynomial-term(int_term_to_ipoly(num)) ≡ num
⊢ ipolynomial-term(minus-poly(int_term_to_ipoly(num))) ≡ "-"num

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}t:int\_term().    ipolynomial-term(int\_term\_to\_ipoly(t))  \mequiv{}  t


By

---

Latex:
xxx(Intro
        THEN  BLemma  `int\_term-induction`
        THEN  Auto
        THEN  Unfold  `int\_term\_to\_ipoly`  0
        THEN  Reduce  0
        THEN  Try  (Fold  `int\_term\_to\_ipoly`  0))xxx

---

Home Index