Nuprl Definition : exact-xover

exact-xover(f;n)==r let a,b = find-xover(f;n;n;1) in if b=a + 1 then a else exact-xover(f;a)

exact-xover(f;n) ==  fix((λexact-xover,n. let b,a = find-xover(f;n;n;1) in if b=a + 1  then a  else (exact-xover a))) n

Definitions occuring in Statement : find-xover: find-xover(f;m;n;step), int_eq: if a=b then c else d, apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, add: n + m, natural_number: $n
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], spread: spread def, find-xover: find-xover(f;m;n;step), int_eq: if a=b then c else d, add: n + m, natural_number: $n, apply: f a
FDL editor aliases : exact-xover

Latex:
exact-xover(f;n)==r let a,b = find-xover(f;n;n;1) in if b=a + 1 then a else exact-xover(f;a)

Latex:
exact-xover(f;n) == fix((\mlambda{}exact-xover,n. let b,a = find-xover(f;n;n;1) in if b=a + 1 then a else (exact-xover a))) n Date html generated: 2016_05_14-AM-07_28_08 Last ObjectModification: 2015_09_22-PM-05_46_25 Theory : int_2 Home Index