P = 2^(t - m') in place of t; the row's sum of P into l, rescaled
317def saExponentials = (lambda unrestricted h : Nat . (lambda unrestricted tail : (family SM86Program) .
318 (saFor 16 (lambda unrestricted i : Nat .
319 (let unrestricted e = (saElem (saS (naturalDivideUnchecked i 2)) h (naturalModuloUnchecked i 2)) in
320 (lambda unrestricted rest : (family SM86Program) .
321 (saFadd e e (saTmp (naturalAdd 6 h)) saWaitNone
322 (saEx2 e e saWaitNone rest)))))
323 -- l = l alpha + (the sum of the sixteen P), once the exponentials are in
324 (saFmul (saL h) (saL h) (saTmp (naturalAdd 4 h)) saWait4
325 (saFor 16 (lambda unrestricted i : Nat .
326 (saFadd (saL h) (saL h) (saElem (saS (naturalDivideUnchecked i 2)) h (naturalModuloUnchecked i 2)) saWaitNone))
327 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.