Nuprl Definition : rep_int_constraint_step

Keep applying as long as the dimension of the "integer problem" is
greater than 0.⋅

rep_int_constraint_step(f;p)==r if (0) < (dim(p))  then let p' ⟵ in rep_int_constraint_step(f;p')  else p

rep_int_constraint_step(f;p) ==
  fix((λrep_int_constraint_step,p. if (0) < (dim(p))  then let p' ⟵ in rep_int_constraint_step p'  else p)) p

Definitions occuring in Statement :  int-problem-dimension: dim(p) callbyvalueall: callbyvalueall less: if (a) < (b)  then c  else d apply: a fix: fix(F) lambda: λx.A[x] natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] less: if (a) < (b)  then c  else d natural_number: $n int-problem-dimension: dim(p) callbyvalueall: callbyvalueall apply: a
FDL editor aliases :  rep_int_constraint_step
==r  if  (0)  <  (dim(p))    then  let  p'  \mleftarrow{}{}  f  p  in  rep\_int\_constraint\_step(f;p')    else  p

rep\_int\_constraint\_step(f;p)  ==
    fix((\mlambda{}rep\_int\_constraint$_{step}$,p.  if  (0)  <  (dim(p))
                                                                          then  let  p'  \mleftarrow{}{}  f  p
                                                                                    in  rep\_int\_constraint$_{step}$  p'
                                                                          else  p)) 

Date html generated: 2016_07_08-PM-04_48_33
Last ObjectModification: 2015_12_14-PM-06_56_22

Theory : omega

Home Index