---

Step * of Lemma rP_to_poly-int_term_to_rP

∀[t:int_term()]. ∀[s:iPolynomial() List].  (rP_to_poly(s;int_term_to_rP(t)) ~ [int_term_to_ipoly(t) / s])
BY
{ Assert ⌜(int_term() ⊆r Base) ∧ ((iPolynomial() List) ⊆r Base)⌝⋅ }

1
.....assertion..... 
(int_term() ⊆r Base) ∧ ((iPolynomial() List) ⊆r Base)

2
1. (int_term() ⊆r Base) ∧ ((iPolynomial() List) ⊆r Base)
⊢ ∀[t:int_term()]. ∀[s:iPolynomial() List].  (rP_to_poly(s;int_term_to_rP(t)) ~ [int_term_to_ipoly(t) / s])

---

Latex:

---

Latex:
\mforall{}[t:int\_term()].  \mforall{}[s:iPolynomial()  List].
    (rP\_to\_poly(s;int\_term\_to\_rP(t))  \msim{}  [int\_term\_to\_ipoly(t)  /  s])


By

---

Latex:
Assert  \mkleeneopen{}(int\_term()  \msubseteq{}r  Base)  \mwedge{}  ((iPolynomial()  List)  \msubseteq{}r  Base)\mkleeneclose{}\mcdot{}

---

Home Index