---

Step * of Lemma assert-rat-term-eq

∀r1,r2:rat_term().
  ((↑rat-term-eq(r1;r2))
  ⇒ (∀f:ℤ ⟶ ℝ. let p,x = rat_term_to_real(f;r1) in let q,y = rat_term_to_real(f;r2) in p ⇒ q ⇒ (x = y)))
BY
{ (InstLemma `rat_term_polynomial` []
   THEN ParallelLast
   THEN (ParallelOp 1 THEN MoveToConcl (-1) THEN MoveToConcl (-2))
   THEN Unfold `rat-term-eq` 0
   THEN GenConclTerms Auto [⌜rat_term_to_ipolys(r1)⌝;⌜rat_term_to_ipolys(r2)⌝]⋅
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN Auto) }

1
1. ∀r:rat_term(). let p,q = rat_term_to_ipolys(r) in r ≡ ipolynomial-term(p)/ipolynomial-term(q)
2. r1 : rat_term()
3. r2 : rat_term()
4. v4 : iPolynomial()
5. v5 : iPolynomial()
6. rat_term_to_ipolys(r1) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
7. v2 : iPolynomial()
8. v3 : iPolynomial()
9. rat_term_to_ipolys(r2) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
10. r1 ≡ ipolynomial-term(v4)/ipolynomial-term(v5)
11. r2 ≡ ipolynomial-term(v2)/ipolynomial-term(v3)
12. ↑null(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))
13. f : ℤ ⟶ ℝ
⊢ let p,x = rat_term_to_real(f;r1) 
  in let q,y = rat_term_to_real(f;r2) 
     in p ⇒ q ⇒ (x = y)

---

Latex:

---

Latex:
\mforall{}r1,r2:rat\_term().
    ((\muparrow{}rat-term-eq(r1;r2))
    {}\mRightarrow{}  (\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
                let  p,x  =  rat\_term\_to\_real(f;r1) 
                in  let  q,y  =  rat\_term\_to\_real(f;r2) 
                      in  p  {}\mRightarrow{}  q  {}\mRightarrow{}  (x  =  y)))


By

---

Latex:
(InstLemma  `rat\_term\_polynomial`  []
  THEN  ParallelLast
  THEN  (ParallelOp  1  THEN  MoveToConcl  (-1)  THEN  MoveToConcl  (-2))
  THEN  Unfold  `rat-term-eq`  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rat\_term\_to\_ipolys(r1)\mkleeneclose{};\mkleeneopen{}rat\_term\_to\_ipolys(r2)\mkleeneclose{}]\mcdot{}
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  Auto)

---

Home Index