accumulators = A (4-register fragments from `a`) x the B fragments, slice
by slice; the first product waits on `first`, each slice after on SB2
580def sqProducts = (lambda unrestricted accumulator : (pi unrestricted nt : Nat . Nat) . (lambda unrestricted a : Nat .
581 (lambda unrestricted first : Nat . (lambda unrestricted tail : (family SM86Program) .
582 (saFor 4 (lambda unrestricted k : Nat .
583 (saFor 8 (lambda unrestricted nt : Nat .
584 (saHmma (accumulator nt) (naturalAdd a (naturalMultiply k 4)) (saB k nt) saSB2
585 (naturalSelect (naturalIsZero nt) (naturalSelect (naturalIsZero k) first saWait2) saWaitNone)))))
586 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.