---

Step * 2 1 of Lemma rP_to_term-int_term_to_rP


1. int_term() ⊆r Base
2. (iPolynomial() List) ⊆r Base
⊢ ∀t:int_term(). ∀s:int_term() List.  (rP_to_term(s;int_term_to_rP(t)) ~ [t / s])
BY
{ Assert ⌜∀t:int_term(). ∀s:int_term() List. ∀L:ℤ List.  (rP_to_term(s;int_term_to_rP(t) @ L) ~ rP_to_term([t / s];L))⌝
⋅ }

1
.....assertion..... 
1. int_term() ⊆r Base
2. (iPolynomial() List) ⊆r Base
⊢ ∀t:int_term(). ∀s:int_term() List. ∀L:ℤ List.  (rP_to_term(s;int_term_to_rP(t) @ L) ~ rP_to_term([t / s];L))

2
1. int_term() ⊆r Base
2. (iPolynomial() List) ⊆r Base
3. ∀t:int_term(). ∀s:int_term() List. ∀L:ℤ List.  (rP_to_term(s;int_term_to_rP(t) @ L) ~ rP_to_term([t / s];L))
⊢ ∀t:int_term(). ∀s:int_term() List.  (rP_to_term(s;int_term_to_rP(t)) ~ [t / s])

---

Latex:

---

Latex:

1.  int\_term()  \msubseteq{}r  Base
2.  (iPolynomial()  List)  \msubseteq{}r  Base
\mvdash{}  \mforall{}t:int\_term().  \mforall{}s:int\_term()  List.    (rP\_to\_term(s;int\_term\_to\_rP(t))  \msim{}  [t  /  s])


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}t:int\_term().  \mforall{}s:int\_term()  List.  \mforall{}L:\mBbbZ{}  List.
                    (rP\_to\_term(s;int\_term\_to\_rP(t)  @  L)  \msim{}  rP\_to\_term([t  /  s];L))\mkleeneclose{}\mcdot{}

---

Home Index