Nuprl Definition : gen_log_aux

gen_log_aux(p;c;x;i;n;M)
==r if M ≤z c * p then n else eval p' = x * p in eval c' = c + i in eval n' = n + 1 in   gen_log_aux(p';c';x;i;n';M) fi 
gen_log_aux(p;c;x;i;n;M) ==
  fix((λgen_log_aux,p,c,n. if M ≤z c * p
                          then n
                          else eval p' = x * p in
                               eval c' = c + i in
                               eval n' = n + 1 in
                                 gen_log_aux p' c' n'
                          fi )) 
  p 
  c 
  n


Definitions occuring in Statement :  callbyvalue: callbyvalue,  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  le_int: i ≤z j,  multiply: n * m,  callbyvalue: callbyvalue,  add: n + m,  natural_number: $n,  apply: f a
FDL editor aliases :  gen_log_aux
Latex:
gen\_log\_aux(p;c;x;i;n;M)
==r  if  M  \mleq{}z  c  *  p
        then  n
        else  eval  p'  =  x  *  p  in
                  eval  c'  =  c  +  i  in
                  eval  n'  =  n  +  1  in
                      gen\_log\_aux(p';c';x;i;n';M)
        fi 

Latex:
gen\_log\_aux(p;c;x;i;n;M)  ==
    fix((\mlambda{}gen\_log$_{aux}$,p,c,n.  if  M  \mleq{}z  c  *  p
                                                  then  n
                                                  else  eval  p'  =  x  *  p  in
                                                            eval  c'  =  c  +  i  in
                                                            eval  n'  =  n  +  1  in
                                                                gen\_log$_{aux}$  p'  c'  n'
                                                  fi  )) 
    p 
    c 
    n


Date html generated: 2018_05_22-PM-03_05_11
Last ObjectModification: 2017_10_25-PM-10_05_46

Theory : reals_2


Home Index