Nuprl Definition : sbcode_aux

sbcode_aux(L;m;n)
==r if (m) < (n)
       then eval n' = n - m in
            sbcode_aux([0 / L];m;n')
       else if (n) < (m)  then eval m' = m - n in sbcode_aux([1 / L];m';n)  else L
sbcode_aux(L;m;n) ==
  fix((λsbcode_aux,L,m,n. if (m) < (n)
                             then eval n' = n - m in
                                  sbcode_aux [0 / L] m n'
                             else if (n) < (m)  then eval m' = m - n in sbcode_aux [1 / L] m' n  else L)) 
  L 
  m 
  n


Definitions occuring in Statement :  cons: [a / b],  callbyvalue: callbyvalue,  less: if (a) < (b)  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  less: if (a) < (b)  then c  else d,  callbyvalue: callbyvalue,  subtract: n - m,  apply: f a,  cons: [a / b],  natural_number: $n
FDL editor aliases :  sbcode_aux
Latex:
sbcode\_aux(L;m;n)
==r  if  (m)  <  (n)
              then  eval  n'  =  n  -  m  in
                        sbcode\_aux([0  /  L];m;n')
              else  if  (n)  <  (m)    then  eval  m'  =  m  -  n  in  sbcode\_aux([1  /  L];m';n)    else  L
Latex:
sbcode\_aux(L;m;n)  ==
    fix((\mlambda{}sbcode$_{aux}$,L,m,n.  if  (m)  <  (n)
                                                        then  eval  n'  =  n  -  m  in
                                                                  sbcode$_{aux}$  [0  /  L]  m  n'
                                                        else  if  (n)  <  (m)
                                                                        then  eval  m'  =  m  -  n  in
                                                                                  sbcode$_{aux}$  [1  /  L]  m'  n
                                                                        else  L)) 
    L 
    m 
    n


Date html generated: 2016_05_15-PM-10_34_02
Last ObjectModification: 2015_09_23-AM-08_26_48

Theory : rationals


Home Index