---

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

.....antecedent..... 
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))
⊢ ↑rat-term-eq(r1;r2)
BY
{ (Fold `it` 4 THEN Fold `btrue` 4) }

1
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))
⊢ ↑rat-term-eq(r1;r2)

---

Latex:

---

Latex:
.....antecedent..... 
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))
\mvdash{}  \muparrow{}rat-term-eq(r1;r2)


By

---

Latex:
(Fold  `it`  4  THEN  Fold  `btrue`  4)

---

Home Index