Nuprl Definition : rep_int_constraint_step
Keep applying f as long as the dimension of the "integer problem" p is
greater than 0.⋅
rep_int_constraint_step(f;p)==r if (0) < (dim(p)) then let p' ⟵ f 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' ⟵ f 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: f 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: f a
FDL editor aliases :
rep_int_constraint_step
Latex:
rep\_int\_constraint\_step(f;p)
==r if (0) < (dim(p)) then let p' \mleftarrow{}{} f p in rep\_int\_constraint\_step(f;p') else p
Latex:
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))
p
Date html generated:
2016_07_08-PM-04_48_33
Last ObjectModification:
2015_12_14-PM-06_56_22
Theory : omega
Home
Index