---

Step * 2 1 2 1 of Lemma rP_to_poly-int_term_to_rP


1. int_term() ⊆r Base
2. (iPolynomial() List) ⊆r Base
3. ∀t:int_term(). ∀s:iPolynomial() List. ∀L:ℤ List.
     (rP_to_poly(s;int_term_to_rP(t) @ L) ~ rP_to_poly([int_term_to_ipoly(t) / s];L))
4. t : int_term()
5. ∀s:iPolynomial() List. ∀L:ℤ List.  (rP_to_poly(s;int_term_to_rP(t) @ L) ~ rP_to_poly([int_term_to_ipoly(t) / s];L))
6. s : iPolynomial() List
7. ∀L:ℤ List. (rP_to_poly(s;int_term_to_rP(t) @ L) ~ rP_to_poly([int_term_to_ipoly(t) / s];L))
⊢ rP_to_poly(s;int_term_to_rP(t)) ~ [int_term_to_ipoly(t) / s]
BY
{ (InstHyp [⌜[]⌝] (-1)⋅ THENA Auto) }

1
1. int_term() ⊆r Base
2. (iPolynomial() List) ⊆r Base
3. ∀t:int_term(). ∀s:iPolynomial() List. ∀L:ℤ List.
     (rP_to_poly(s;int_term_to_rP(t) @ L) ~ rP_to_poly([int_term_to_ipoly(t) / s];L))
4. t : int_term()
5. ∀s:iPolynomial() List. ∀L:ℤ List.  (rP_to_poly(s;int_term_to_rP(t) @ L) ~ rP_to_poly([int_term_to_ipoly(t) / s];L))
6. s : iPolynomial() List
7. ∀L:ℤ List. (rP_to_poly(s;int_term_to_rP(t) @ L) ~ rP_to_poly([int_term_to_ipoly(t) / s];L))
8. rP_to_poly(s;int_term_to_rP(t) @ []) ~ rP_to_poly([int_term_to_ipoly(t) / s];[])
⊢ rP_to_poly(s;int_term_to_rP(t)) ~ [int_term_to_ipoly(t) / s]

---

Latex:

---

Latex:

1.  int\_term()  \msubseteq{}r  Base
2.  (iPolynomial()  List)  \msubseteq{}r  Base
3.  \mforall{}t:int\_term().  \mforall{}s:iPolynomial()  List.  \mforall{}L:\mBbbZ{}  List.
          (rP\_to\_poly(s;int\_term\_to\_rP(t)  @  L)  \msim{}  rP\_to\_poly([int\_term\_to\_ipoly(t)  /  s];L))
4.  t  :  int\_term()
5.  \mforall{}s:iPolynomial()  List.  \mforall{}L:\mBbbZ{}  List.
          (rP\_to\_poly(s;int\_term\_to\_rP(t)  @  L)  \msim{}  rP\_to\_poly([int\_term\_to\_ipoly(t)  /  s];L))
6.  s  :  iPolynomial()  List
7.  \mforall{}L:\mBbbZ{}  List.  (rP\_to\_poly(s;int\_term\_to\_rP(t)  @  L)  \msim{}  rP\_to\_poly([int\_term\_to\_ipoly(t)  /  s];L))
\mvdash{}  rP\_to\_poly(s;int\_term\_to\_rP(t))  \msim{}  [int\_term\_to\_ipoly(t)  /  s]


By

---

Latex:
(InstHyp  [\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)

---

Home Index