Nuprl Definition : rmul
a * b == eval a1 = a in eval b1 = b in accelerate(imax(|a1 1|;|b1 1|) + 4;reg-seq-mul(a1;b1))
Definitions occuring in Statement :
reg-seq-mul: reg-seq-mul(x;y),
accelerate: accelerate(k;f),
imax: imax(a;b),
absval: |i|,
callbyvalue: callbyvalue,
apply: f a,
add: n + m,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
accelerate: accelerate(k;f),
add: n + m,
imax: imax(a;b),
absval: |i|,
apply: f a,
natural_number: $n,
reg-seq-mul: reg-seq-mul(x;y)
FDL editor aliases :
rmul
Latex:
a * b == eval a1 = a in eval b1 = b in accelerate(imax(|a1 1|;|b1 1|) + 4;reg-seq-mul(a1;b1))
Date html generated:
2019_10_16-PM-03_06_52
Last ObjectModification:
2019_01_31-PM-04_49_22
Theory : reals
Home
Index