P = 2^(t - m') in place of t; the row's sum of P into l, rescaled
302def saExponentials = (lambda unrestricted h : Nat . (lambda unrestricted tail : (family SM86Program) .
303 (saFor 16 (lambda unrestricted i : Nat .
304 (let unrestricted e = (saElem (saS (naturalDivideUnchecked i 2)) h (naturalModuloUnchecked i 2)) in
305 (lambda unrestricted rest : (family SM86Program) .
306 (saFadd e e (saTmp (naturalAdd 6 h)) saWaitNone
307 (saEx2 e e saWaitNone rest)))))
308 -- l = l alpha + (the sum of the sixteen P), once the exponentials are in
309 (saFmul (saL h) (saL h) (saTmp (naturalAdd 4 h)) saWait4
310 (saFor 16 (lambda unrestricted i : Nat .
311 (saFadd (saL h) (saL h) (saElem (saS (naturalDivideUnchecked i 2)) h (naturalModuloUnchecked i 2)) saWaitNone))
312 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.