P's A fragments for P V: k-slice kk is n-tiles 2 kk and 2 kk + 1
311def saPackP = (lambda unrestricted tail : (family SM86Program) .
312 (saFor 4 (lambda unrestricted kk : Nat .
313 (let unrestricted left = (saS (naturalMultiply 2 kk)) in (let unrestricted right = (saS (succ (naturalMultiply 2 kk))) in
314 (lambda unrestricted rest : (family SM86Program) .
315 (saPack (saPA kk) (succ left) left
316 (saPack (succ (saPA kk)) (naturalAdd left 3) (naturalAdd left 2)
317 (saPack (naturalAdd (saPA kk) 2) (succ right) right
318 (saPack (naturalAdd (saPA kk) 3) (naturalAdd right 3) (naturalAdd right 2)
319 rest))))))))
320 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.