---

Step * 2 of Lemma rP_to_term-int_term_to_rP


1. (int_term() ⊆r Base) ∧ ((iPolynomial() List) ⊆r Base)
⊢ ∀[t:int_term()]. ∀[s:int_term() List].  (rP_to_term(s;int_term_to_rP(t)) ~ [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:int_term() List.  (rP_to_term(s;int_term_to_rP(t)) ~ [t / s])

---

Latex:

---

Latex:

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

---

Home Index