---

Step * 1 1 of Lemma qeq-qrep


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
BY
{ xxx((InstLemma `gcd_reduce_property` [⌜a2⌝;⌜a3⌝]⋅ THENA Auto)
      THEN (MoveToConcl (-1))
      THEN (GenConclAtAddr [1;1] THENA Auto)
      THEN (Thin (-1))
      THEN RepeatFor 2 (D -1)
      THEN Reduce 0
      THEN AutoBoolCase ⌜0 ≤z v4⌝⋅)xxx }

---

Latex:

---

Latex:

1.  a2  :  \mBbbZ{}
2.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  if  isint(let  g,a,b  =  gcd\_reduce(a2;a3)  in 
          if  0  \mleq{}z  b  then  <a,  b>  else  <-a,  -b>  fi  )
    then  (a2  =\msubz{}  let  g,a,b  =  gcd\_reduce(a2;a3)  in  if  0  \mleq{}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  \mleq{}z  b  then  <a,  b>  else  <-a,  -b>  fi   
              in  (a2  *  j  =\msubz{}  i  *  a3)
    fi   
=  tt


By

---

Latex:
xxx((InstLemma  `gcd\_reduce\_property`  [\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}a3\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (MoveToConcl  (-1))
        THEN  (GenConclAtAddr  [1;1]  THENA  Auto)
        THEN  (Thin  (-1))
        THEN  RepeatFor  2  (D  -1)
        THEN  Reduce  0
        THEN  AutoBoolCase  \mkleeneopen{}0  \mleq{}z  v4\mkleeneclose{}\mcdot{})xxx

---

Home Index