P = 2^(t - m') in place of t; the row's sum of P into l, rescaled
290def saExponentials = (lambda unrestricted h : Nat . (lambda unrestricted tail : (family SM86Program) .
291 (saFor 16 (lambda unrestricted i : Nat .
292 (let unrestricted e = (saElem (saS (naturalDivideUnchecked i 2)) h (naturalModuloUnchecked i 2)) in
293 (lambda unrestricted rest : (family SM86Program) .
294 (saFadd e e (saTmp (naturalAdd 6 h)) saWaitNone
295 (saEx2 e e saWaitNone rest)))))
296 -- l = l alpha + (the sum of the sixteen P), once the exponentials are in
297 (saFmul (saL h) (saL h) (saTmp (naturalAdd 4 h)) saWait4
298 (saFor 16 (lambda unrestricted i : Nat .
299 (saFadd (saL h) (saL h) (saElem (saS (naturalDivideUnchecked i 2)) h (naturalModuloUnchecked i 2)) saWaitNone))
300 tail)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.