---

Step * 1 of Lemma rounded-numerator_wf


1. k : ℕ+
2. v : ℤ ⋃ (ℤ × ℤ-o)
3. v1 : ℤ ⋃ (ℤ × ℤ-o)
4. qeq(v;v1) = tt
⊢ rounded-numerator(v;k) = rounded-numerator(v1;k) ∈ ℤ
BY
{ xxx(Unfold `qeq` (-1)
      THEN RepeatFor 2 ((CallByValueReduce (-1) THENA Auto))
      THEN Unfold `rounded-numerator` 0
      THEN (CallByValueReduce 0 THENA Auto)
      THEN All D_rational_form
      THEN Auto
      THEN (RWO "eqtt_to_assert" (-1) THENA Auto)
      THEN (RW assert_pushdownC (-1) THENA Auto))xxx }

1
1. k : ℕ+
2. a3 : ℤ
3. a4 : ℤ-o
4. a1 : ℤ
5. a3 = (a1 * a4) ∈ ℤ
⊢ ((a3 * k) ÷ a4) = (a1 * k) ∈ ℤ

2
1. k : ℕ+
2. a4 : ℤ
3. a2 : ℤ
4. a3 : ℤ-o
5. (a4 * a3) = a2 ∈ ℤ
⊢ (a4 * k) = ((a2 * k) ÷ a3) ∈ ℤ

3
1. k : ℕ+
2. a5 : ℤ
3. a6 : ℤ-o
4. a2 : ℤ
5. a3 : ℤ-o
6. (a5 * a3) = (a2 * a6) ∈ ℤ
⊢ ((a5 * k) ÷ a6) = ((a2 * k) ÷ a3) ∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  v  :  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
3.  v1  :  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
4.  qeq(v;v1)  =  tt
\mvdash{}  rounded-numerator(v;k)  =  rounded-numerator(v1;k)


By

---

Latex:
xxx(Unfold  `qeq`  (-1)
        THEN  RepeatFor  2  ((CallByValueReduce  (-1)  THENA  Auto))
        THEN  Unfold  `rounded-numerator`  0
        THEN  (CallByValueReduce  0  THENA  Auto)
        THEN  All  D\_rational\_form
        THEN  Auto
        THEN  (RWO  "eqtt\_to\_assert"  (-1)  THENA  Auto)
        THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))xxx

---

Home Index