---

Step * of Lemma equipollent-nat-rationals-ext

ℕ ~ ℚ
BY
{ Extract of Obid: equipollent-nat-rationals
  not unfolding  mu qrep enumerate coded-pair is-qrep primrec
  finishing with (Auto THEN Fold `bottom` 0 THEN Auto)
  normalizes to:
  
  <λx.let a,b = coded-pair(primrec(x;mu(λn.if is-qrep(let a,b = coded-pair(n) 
                                                      in <let q,r = divrem(b; 2) 
                                                          in if r=0 then q else (-(q + 1))
                                                         , a + 1
                                                         >)
                                           then inl Ax
                                           else inr Ax 
                                           fi );λi,r. eval r' = r + 1 in
                                                      r'
                                                      + mu(λk.if is-qrep(let a,b = coded-pair(r' + k) 
                                                                         in <let q,r = divrem(b; 2) 
                                                                             in if r=0 then q else (-(q + 1))
                                                                            , a + 1
                                                                            >)
                                                              then inl Ax
                                                              else inr Ax 
                                                              fi ))) 
      in <let q,r = divrem(b; 2) in if r=0 then q else (-(q + 1)), a + 1>
  , λa1,a2,%. Ax
  , λb.let x,y = qrep(b) 
       in if is-qrep(let a,b = coded-pair(let q,y1 = divrem(((y - 1)
                                                            + if (x) < (0)  then (2 * ((-x) - 1)) + 1  else (2 * x))
                                                            * (((y - 1)
                                                              + if (x) < (0)  then (2 * ((-x) - 1)) + 1  else (2 * x))
                                                              + 1);
                                                            2) 
                                          in q + (y - 1)) 
                     in <let q,r = divrem(b; 2) in if r=0 then q else (-(q + 1)), a + 1>)
          then <primrec(let q,y1 = divrem(((y - 1) + if (x) < (0)  then (2 * ((-x) - 1)) + 1  else (2 * x))
                                          * (((y - 1) + if (x) < (0)  then (2 * ((-x) - 1)) + 1  else (2 * x)) + 1);
                                          2) 
                        in q + (y - 1);0;λn,m. if is-qrep(let a,b = coded-pair(n) 
                                                          in <let q,r = divrem(b; 2) 
                                                              in if r=0 then q else (-(q + 1))
                                                             , a + 1
                                                             >)
                                              then 1 + m
                                              else 0 + m
                                              fi )
               , Ax
               >
          else let a@0,%10 = ⊥ 
               in <a@0, Ax>
          fi > }

---

Latex:

---

Latex:
\mBbbN{}  \msim{}  \mBbbQ{}


By

---

Latex:
Extract  of  Obid:  equipollent-nat-rationals
not  unfolding    mu  qrep  enumerate  coded-pair  is-qrep  primrec
finishing  with  (Auto  THEN  Fold  `bottom`  0  THEN  Auto)
normalizes  to:

<\mlambda{}x.let  a,b  =  coded-pair(primrec(x;mu(\mlambda{}n.if  is-qrep(let  a,b  =  coded-pair(n) 
                                                                                                        in  <let  q,r  =  divrem(b;  2) 
                                                                                                                in  if  r=0  then  q  else  (-(q  +  1))
                                                                                                              ,  a  +  1
                                                                                                              >)
                                                                                  then  inl  Ax
                                                                                  else  inr  Ax 
                                                                                  fi  );\mlambda{}i,r.  eval  r'  =  r  +  1  in
                                                                                                        r'
                                                                                                        +  mu(\mlambda{}k.if  is-qrep(let  a,b  =  coded-pair(r'  +  k) 
                                                                                                                                              in  <let  q,r  =  divrem(b;  2) 
                                                                                                                                                      in  if  r=0
                                                                                                                                                            then  q
                                                                                                                                                            else  (-(q  +  1))
                                                                                                                                                    ,  a  +  1
                                                                                                                                                    >)
                                                                                                                        then  inl  Ax
                                                                                                                        else  inr  Ax 
                                                                                                                        fi  ))) 
        in  <let  q,r  =  divrem(b;  2)  in  if  r=0  then  q  else  (-(q  +  1)),  a  +  1>
,  \mlambda{}a1,a2,\%.  Ax
,  \mlambda{}b.let  x,y  =  qrep(b) 
          in  if  is-qrep(let  a,b  =  coded-pair(let  q,y1  =  divrem(((y  -  1)
                                                                                                                    +  if  (x)  <  (0)
                                                                                                                              then  (2  *  ((-x)  -  1))  +  1
                                                                                                                              else  (2  *  x))
                                                                                                                    *  (((y  -  1)
                                                                                                                        +  if  (x)  <  (0)
                                                                                                                                  then  (2  *  ((-x)  -  1))  +  1
                                                                                                                                  else  (2  *  x))
                                                                                                                        +  1);
                                                                                                                    2) 
                                                                                in  q  +  (y  -  1)) 
                                      in  <let  q,r  =  divrem(b;  2)  in  if  r=0  then  q  else  (-(q  +  1)),  a  +  1>)
                then  <primrec(let  q,y1  =  divrem(((y  -  1)
                                                                                +  if  (x)  <  (0)    then  (2  *  ((-x)  -  1))  +  1    else  (2  *  x))
                                                                                *  (((y  -  1)
                                                                                    +  if  (x)  <  (0)    then  (2  *  ((-x)  -  1))  +  1    else  (2  *  x))
                                                                                    +  1);
                                                                                2) 
                                            in  q  +  (y  -  1);0;\mlambda{}n,m.  if  is-qrep(let  a,b  =  coded-pair(n) 
                                                                                                                in  <let  q,r  =  divrem(b;  2) 
                                                                                                                        in  if  r=0  then  q  else  (-(q  +  1))
                                                                                                                      ,  a  +  1
                                                                                                                      >)
                                                                                        then  1  +  m
                                                                                        else  0  +  m
                                                                                        fi  )
                          ,  Ax
                          >
                else  let  a@0,\%10  =  \mbot{} 
                          in  <a@0,  Ax>
                fi  >

---

Home Index