---

Step * of Lemma assert-rat-term-eq2

∀[r1,r2:rat_term()]. ∀[f:ℤ ⟶ ℝ].
  ((snd(rat_term_to_real(f;r1))) = (snd(rat_term_to_real(f;r2)))) supposing 
     ((fst(rat_term_to_real(f;r1))) and 
     (fst(rat_term_to_real(f;r2))) and 
     (inl Ax ≤ rat-term-eq(r1;r2)))
BY
{ (RepeatFor 6 (Intro) THEN (Unhide THENA Auto) THEN (InstLemma `assert-rat-term-eq` [⌜r1⌝;⌜r2⌝;⌜f⌝]⋅ THENA Auto)) }

1
.....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)

2
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)))

---

Latex:

---

Latex:
\mforall{}[r1,r2:rat\_term()].  \mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}].
    ((snd(rat\_term\_to\_real(f;r1)))  =  (snd(rat\_term\_to\_real(f;r2))))  supposing 
          ((fst(rat\_term\_to\_real(f;r1)))  and 
          (fst(rat\_term\_to\_real(f;r2)))  and 
          (inl  Ax  \mleq{}  rat-term-eq(r1;r2)))


By

---

Latex:
(RepeatFor  6  (Intro)
  THEN  (Unhide  THENA  Auto)
  THEN  (InstLemma  `assert-rat-term-eq`  [\mkleeneopen{}r1\mkleeneclose{};\mkleeneopen{}r2\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index