---

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


1. r1 : rat_term()
2. r2 : rat_term()
3. f : ℤ ⟶ ℝ
4. tt ≤ rat-term-eq(r1;r2)
5. fst(rat_term_to_real(f;r2))
6. fst(rat_term_to_real(f;r1))
7. mono(𝔹)
⊢ ↑rat-term-eq(r1;r2)
BY
{ ((D -1 With ⌜tt⌝  THENA Auto) THEN InstHyp [⌜rat-term-eq(r1;r2)⌝] (-1)⋅ THEN Auto THEN D 0 With ⌜tt⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  r1  :  rat\_term()
2.  r2  :  rat\_term()
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
4.  tt  \mleq{}  rat-term-eq(r1;r2)
5.  fst(rat\_term\_to\_real(f;r2))
6.  fst(rat\_term\_to\_real(f;r1))
7.  mono(\mBbbB{})
\mvdash{}  \muparrow{}rat-term-eq(r1;r2)


By

---

Latex:
((D  -1  With  \mkleeneopen{}tt\mkleeneclose{}    THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}rat-term-eq(r1;r2)\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}tt\mkleeneclose{} 
  THEN  Auto)

---

Home Index