P's A fragments for P V: k-slice kk is n-tiles 2 kk and 2 kk + 1
338def saPackP = (lambda unrestricted tail : (family SM86Program) .
339 (saFor 4 (lambda unrestricted kk : Nat .
340 (let unrestricted left = (saS (naturalMultiply 2 kk)) in (let unrestricted right = (saS (succ (naturalMultiply 2 kk))) in
341 (lambda unrestricted rest : (family SM86Program) .
342 (saPack (saPA kk) (succ left) left
343 (saPack (succ (saPA kk)) (naturalAdd left 3) (naturalAdd left 2)
344 (saPack (naturalAdd (saPA kk) 2) (succ right) right
345 (saPack (naturalAdd (saPA kk) 3) (naturalAdd right 3) (naturalAdd right 2)
346 rest))))))))
347 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.