---

Step * of Lemma qrep_wf

No Annotations
∀[r:ℚ]. (qrep(r) ∈ ℤ × ℕ+)
BY
{ (Auto
   THEN D 1
   THEN MoveToConcl (-1)
   THEN (GenConclTerms Auto [⌜r⌝;⌜r1⌝]⋅ THENA Auto)
   THEN All Thin
   THEN (D 0 THENA Auto)
   THEN All D_rational_form
   THEN MoveToConcl (-1)
   THEN RepUR ``qeq qrep`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (Reduce 0 THENA Auto)
   THEN All Thin
   THEN ((RWO "eqtt_to_assert" 0 THENM RW assert_pushdownC 0) THENA Auto)) }

1
1. a2 : ℤ
2. a1 : ℤ
⊢ (a2 = a1 ∈ ℤ) ⇒ (<a2, 1> = <a1, 1> ∈ (ℤ × ℕ+))

2
1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
⊢ (a3 = (a1 * a4) ∈ ℤ)
⇒ (let g,a,b = gcd_reduce(a3;a4) in if 0 ≤z b then <a, b> else <-a, -b> fi  = <a1, 1> ∈ (ℤ × ℕ+))

3
1. a4 : ℤ
2. a2 : ℤ
3. a3 : ℤ-o
⊢ ((a4 * a3) = a2 ∈ ℤ) ⇒ (<a4, 1> = let g,a,b = gcd_reduce(a2;a3) in if 0 ≤z b then <a, b> else <-a, -b> fi  ∈ (ℤ × ℕ+)\000C)

4
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
⊢ ((a5 * a3) = (a2 * a6) ∈ ℤ)
⇒ (let g,a,b = gcd_reduce(a5;a6) in 
   if 0 ≤z b then <a, b> else <-a, -b> fi 
   = let g,a,b = gcd_reduce(a2;a3) in 
     if 0 ≤z b then <a, b> else <-a, -b> fi 
   ∈ (ℤ × ℕ+))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:\mBbbQ{}].  (qrep(r)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})


By

---

Latex:
(Auto
  THEN  D  1
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerms  Auto  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  (D  0  THENA  Auto)
  THEN  All  D\_rational\_form
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``qeq  qrep``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (Reduce  0  THENA  Auto)
  THEN  All  Thin
  THEN  ((RWO  "eqtt\_to\_assert"  0  THENM  RW  assert\_pushdownC  0)  THENA  Auto))

---

Home Index