---

Step * of Lemma chinese-remainder2-extract

∀r,s,a,b:ℤ.  Dec(∃x:ℤ [((x ≡ a mod r) ∧ (x ≡ b mod s))])
BY
{ Extract of Obid: chinese-remainder2
  not unfolding  absval
  finishing with Auto
  normalizes to:
  
  λr,s,a,b. let x,y = 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,%13 = rec r p 
                                               in let a,b,x1,y1,%18,%20,%21 = %13 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(|r|) 
                      |s| 
            in let x1,x2,x3,x4,x5,x5,y = y in 
                if x=0
                then if a=b then inl a else (inr (λx.Ax) )
                else let x4,r1 = divrem(b - a; x) 
                     in if r1=0
                        then eval z = a + if (r) < (0)  then ((-1) * x3) * x4 * r  else ((1 * x3) * x4 * r) in
                             inl z
                        else (inr (λx.Ax) ) }

---

Latex:

---

Latex:
\mforall{}r,s,a,b:\mBbbZ{}.    Dec(\mexists{}x:\mBbbZ{}  [((x  \mequiv{}  a  mod  r)  \mwedge{}  (x  \mequiv{}  b  mod  s))])


By

---

Latex:
Extract  of  Obid:  chinese-remainder2
not  unfolding    absval
finishing  with  Auto
normalizes  to:

\mlambda{}r,s,a,b.  let  x,y  =  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,\%13  =  rec  r  p 
                                                                                          in  let  a,b,x1,y1,\%18,\%20,\%21  =  \%13  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(|r|) 
                                        |s| 
                    in  let  x1,x2,x3,x4,x5,x5,y  =  y  in 
                            if  x=0
                            then  if  a=b  then  inl  a  else  (inr  (\mlambda{}x.Ax)  )
                            else  let  x4,r1  =  divrem(b  -  a;  x) 
                                      in  if  r1=0
                                            then  eval  z  =  a
                                                      +  if  (r)  <  (0)    then  ((-1)  *  x3)  *  x4  *  r    else  ((1  *  x3)  *  x4  *  r)  in
                                                      inl  z
                                            else  (inr  (\mlambda{}x.Ax)  )

---

Home Index