slice k's products into `scores`, as sfScores's (from RZ at k = 0): the
first after the slice's fragments (SB1) and, past k = 0, the previous
slice's products (SB2)
987def sfpScoreSlice = (lambda unrestricted guard : Nat . (lambda unrestricted scores : (pi unrestricted nt : Nat . Nat) .
988 (lambda unrestricted k : Nat . (lambda unrestricted tail : (family SM86Program) .
989 (saFor 8 (lambda unrestricted nt : Nat .
990 (sfpOp guard (sfpHmma (scores nt) (saQ k) (sfpB k nt)
991 (naturalSelect (naturalIsZero k) sm86RegisterZero (scores nt)) saSB2
992 (naturalSelect (naturalIsZero nt) (naturalSelect (naturalIsZero k) saWait1 (naturalAdd saWait1 saWait2)) saWaitNone))))
993 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.