---

Step * of Lemma real_term_polynomial

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

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

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

3
1. left : int_term()
2. right : int_term()
3. ipolynomial-term(int_term_to_ipoly(left)) ≡ left
4. 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. left : int_term()
2. right : int_term()
3. ipolynomial-term(int_term_to_ipoly(left)) ≡ left
4. 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. left : int_term()
2. right : int_term()
3. ipolynomial-term(int_term_to_ipoly(left)) ≡ left
4. 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. num : int_term()
2. ipolynomial-term(int_term_to_ipoly(num)) ≡ num
⊢ ipolynomial-term(minus-poly(int_term_to_ipoly(num))) ≡ "-"num

---

Latex:

---

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


By

---

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

---

Home Index