---

Step * 2 of Lemma rP_to_poly-int_term_to_rP


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])
BY
{ (D -1 THEN Intros THEN UseWitness ⌜Ax⌝⋅ THEN MemCD THEN RepeatFor 2 (MoveToConcl (-1))) }

1
1. int_term() ⊆r Base
2. (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:

1.  (int\_term()  \msubseteq{}r  Base)  \mwedge{}  ((iPolynomial()  List)  \msubseteq{}r  Base)
\mvdash{}  \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:
(D  -1  THEN  Intros  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  MemCD  THEN  RepeatFor  2  (MoveToConcl  (-1)))

---

Home Index