Nuprl Definition : sbcode
sbcode(m;n)==r if (m) < (n) then [0 / sbcode(m;n - m)] else if (n) < (m) then [1 / sbcode(m - n;n)] else []
sbcode(m;n) ==
fix((λsbcode,m,n. if (m) < (n)
then [0 / (sbcode m (n - m))]
else if (n) < (m) then [1 / (sbcode (m - n) n)] else []))
m
n
Definitions occuring in Statement :
cons: [a / b],
nil: [],
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,
cons: [a / b],
natural_number: $n,
apply: f a,
subtract: n - m,
nil: []
FDL editor aliases :
sbcode
Latex:
sbcode(m;n)
==r if (m) < (n) then [0 / sbcode(m;n - m)] else if (n) < (m) then [1 / sbcode(m - n;n)] else []
Latex:
sbcode(m;n) ==
fix((\mlambda{}sbcode,m,n. if (m) < (n)
then [0 / (sbcode m (n - m))]
else if (n) < (m) then [1 / (sbcode (m - n) n)] else []))
m
n
Date html generated:
2016_05_15-PM-10_33_59
Last ObjectModification:
2015_09_23-AM-08_26_47
Theory : rationals
Home
Index