a product's program with tile t: looped 1 the loop, 0 the checked
unrolling (Proof.GB10TiledChoiceProbe times every candidate this way)
578def coppeliusTiledProgramWith = (lambda unrestricted t : (family TiledProductTile) .
579 (lambda unrestricted looped : Nat . (lambda unrestricted residual : Nat .
580 (lambda unrestricted a : (family TiledProductLayout) . (lambda unrestricted b : (family TiledProductLayout) .
581 (lambda unrestricted m : Nat . (lambda unrestricted n : Nat . (lambda unrestricted k : Nat .
582 (let unrestricted sa = (coppeliusTiledStrideA a m k) in (let unrestricted sb = (coppeliusTiledStrideB b n k) in
583 (eliminate StdBool (lambda unrestricted c : (family StdBool) . (family SM86Program)) (stdBoolFromNatural looped)
584 (branch StdTrue .
585 (eliminate StdBool (lambda unrestricted c : (family StdBool) . (family SM86Program)) (stdBoolFromNatural residual)
586 (branch StdTrue . (tiledProductSM86Residual sm86CompactStallsDrained t a b k sa sb n))
587 (branch StdFalse . (tiledProductSM86 sm86CompactStallsDrained t a b k sa sb n))))
588 (branch StdFalse .
589 (eliminate StdBool (lambda unrestricted c : (family StdBool) . (family SM86Program)) (stdBoolFromNatural residual)
590 (branch StdTrue . (tiledProductSM86ResidualChecked sm86CompactStallsDrained t a b k sa sb n))
591 (branch StdFalse . (tiledProductSM86Checked sm86CompactStallsDrained t a b k sa sb n)))))))))))))))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.