---

Step * 2 of Lemma assert-rat-term-eq2


1. r1 : rat_term()
2. r2 : rat_term()
3. f : ℤ ⟶ ℝ
4. inl Ax ≤ rat-term-eq(r1;r2)
5. fst(rat_term_to_real(f;r2))
6. fst(rat_term_to_real(f;r1))
7. let p,x = rat_term_to_real(f;r1) 
   in let q,y = rat_term_to_real(f;r2) 
      in p ⇒ q ⇒ (x = y)
⊢ (snd(rat_term_to_real(f;r1))) = (snd(rat_term_to_real(f;r2)))
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜rat_term_to_real(f;r1)⌝;⌜rat_term_to_real(f;r2)⌝]⋅
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  r1  :  rat\_term()
2.  r2  :  rat\_term()
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
4.  inl  Ax  \mleq{}  rat-term-eq(r1;r2)
5.  fst(rat\_term\_to\_real(f;r2))
6.  fst(rat\_term\_to\_real(f;r1))
7.  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)
\mvdash{}  (snd(rat\_term\_to\_real(f;r1)))  =  (snd(rat\_term\_to\_real(f;r2)))


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rat\_term\_to\_real(f;r1)\mkleeneclose{};\mkleeneopen{}rat\_term\_to\_real(f;r2)\mkleeneclose{}]\mcdot{}
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  Auto)

---

Home Index