---

Step * of Lemma gcd-reduce-ext

∀p,q:ℤ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
BY
{ Extract of Obid: gcd-reduce
  not unfolding  sign absval
  finishing with Auto
  normalizes to:
  
  λp,q. let g,t = letrec rec(p)=λq.if p=0
                                   then <q, 0, 1, 1, 1, Ax, Ax, Ax>
                                   else let x,y = divrem(q; p) 
                                        in eval r = y in
                                           let g,t = rec r p 
                                           in let a,b,x1,y1,_,_,_ = t in 
                                               eval q' = x in
                                               eval b' = (b * q') + a in
                                               eval x' = y1 - x1 * q' in
                                                 <g, b, b', x', x1, Ax, Ax, Ax> in
                   rec(|p|) 
                  |q| 
        in let a,b,x,y,_,_,_ = t in 
            <g, sign(p) * a, sign(q) * b, sign(p) * x, sign(q) * y, Ax, Ax, Ax> }

---

Latex:

---

Latex:
\mforall{}p,q:\mBbbZ{}.    \mexists{}g:\mBbbN{}.  \mexists{}a,b,x,y:\mBbbZ{}.  ((p  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  (((x  *  a)  +  (y  *  b))  =  1))


By

---

Latex:
Extract  of  Obid:  gcd-reduce
not  unfolding    sign  absval
finishing  with  Auto
normalizes  to:

\mlambda{}p,q.  let  g,t  =  letrec  rec(p)=\mlambda{}q.if  p=0
                                                                  then  <q,  0,  1,  1,  1,  Ax,  Ax,  Ax>
                                                                  else  let  x,y  =  divrem(q;  p) 
                                                                            in  eval  r  =  y  in
                                                                                  let  g,t  =  rec  r  p 
                                                                                  in  let  a,b,x1,y1,$_{}$,$_{\mbackslash{}\000Cff7d$,$_{}$  =  t  in 
                                                                                          eval  q'  =  x  in
                                                                                          eval  b'  =  (b  *  q')  +  a  in
                                                                                          eval  x'  =  y1  -  x1  *  q'  in
                                                                                              <g,  b,  b',  x',  x1,  Ax,  Ax,  Ax>  in
                                  rec(|p|) 
                                |q| 
            in  let  a,b,x,y,$_{}$,$_{}$,$_{}$  =\000C  t  in 
                    <g,  sign(p)  *  a,  sign(q)  *  b,  sign(p)  *  x,  sign(q)  *  y,  Ax,  Ax,  Ax>

---

Home Index