---

Step * 1 of Lemma rat-int-part_wf2


1. q : Base
2. q1 : Base
3. q = q1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
4. q ∈ ℤ ⋃ (ℤ × ℤ-o)
5. q1 ∈ ℤ ⋃ (ℤ × ℤ-o)
6. qeq(q;q1) = tt
⊢ rat-int-part(q) = rat-int-part(q1) ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} 
BY
{ (GenConclAtAddr [2]
   THEN GenConclAtAddr [3]
   THEN RepeatFor 2 (DVar `v')
   THEN RepeatFor 2 (DVar `v1')
   THEN All Reduce
   THEN EqTypeCD
   THEN Reduce 0
   THEN Auto
   THEN DVar `v3'
   THEN DVar `v5'
   THEN (Assert q = q1 ∈ ℚ BY
               (EqTypeCD THEN Auto))
   THEN (Assert (v2 + v3) = (v4 + v5) ∈ ℚ BY
               Auto)) }

1
1. q : Base
2. q1 : Base
3. q = q1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
4. q ∈ ℤ ⋃ (ℤ × ℤ-o)
5. q1 ∈ ℤ ⋃ (ℤ × ℤ-o)
6. qeq(q;q1) = tt
7. v2 : ℤ
8. v3 : ℚ
9. (0 ≤ v3) ∧ v3 < 1
10. q = (v2 + v3) ∈ ℚ
11. rat-int-part(q) = <v2, v3> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} 
12. v4 : ℤ
13. v5 : ℚ
14. (0 ≤ v5) ∧ v5 < 1
15. q1 = (v4 + v5) ∈ ℚ
16. rat-int-part(q1) = <v4, v5> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q1 = (x + r) ∈ ℚ} 
17. q = q1 ∈ ℚ
18. (v2 + v3) = (v4 + v5) ∈ ℚ
⊢ <v2, v3> = <v4, v5> ∈ (ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} )

---

Latex:

---

Latex:

1.  q  :  Base
2.  q1  :  Base
3.  q  =  q1
4.  q  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
5.  q1  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
6.  qeq(q;q1)  =  tt
\mvdash{}  rat-int-part(q)  =  rat-int-part(q1)


By

---

Latex:
(GenConclAtAddr  [2]
  THEN  GenConclAtAddr  [3]
  THEN  RepeatFor  2  (DVar  `v')
  THEN  RepeatFor  2  (DVar  `v1')
  THEN  All  Reduce
  THEN  EqTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  DVar  `v3'
  THEN  DVar  `v5'
  THEN  (Assert  q  =  q1  BY
                          (EqTypeCD  THEN  Auto))
  THEN  (Assert  (v2  +  v3)  =  (v4  +  v5)  BY
                          Auto))

---

Home Index