---

Step * 1 of Lemma qeq-qrep


1. v : ℤ ⋃ (ℤ × ℤ-o)
⊢ qeq(v;qrep(v)) = tt
BY
{ xxx(xxxD_rational_form 1xxx
      THEN (RepUR ``qeq qrep`` 0 THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))⋅ THEN Reduce 0 THEN Auto)
      THEN Try (Complete ((GenConclAtAddr [2;1;1] THEN RepeatFor 2 (D -2) THEN Reduce 0 THEN AutoSplit THEN Auto)))
      THEN Try (Complete (Auto)))xxx }

1
1. a2 : ℤ
2. a3 : ℤ-o
⊢ if isint(let g,a,b = gcd_reduce(a2;a3) in 
     if 0 ≤z b then <a, b> else <-a, -b> fi )
  then (a2 =z let g,a,b = gcd_reduce(a2;a3) in if 0 ≤z b then <a, b> else <-a, -b> fi  * a3)
  else let i,j = let g,a,b = gcd_reduce(a2;a3) in 
       if 0 ≤z b then <a, b> else <-a, -b> fi  
       in (a2 * j =z i * a3)
  fi  
= tt

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
\mvdash{}  qeq(v;qrep(v))  =  tt


By

---

Latex:
xxx(xxxD\_rational\_form  1xxx
        THEN  (RepUR  ``qeq  qrep``  0
                    THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))\mcdot{}
                    THEN  Reduce  0
                    THEN  Auto)
        THEN  Try  (Complete  ((GenConclAtAddr  [2;1;1]
                                                  THEN  RepeatFor  2  (D  -2)
                                                  THEN  Reduce  0
                                                  THEN  AutoSplit
                                                  THEN  Auto)))
        THEN  Try  (Complete  (Auto)))xxx

---

Home Index