649def niRunAdmitted =
650 (lambda unrestricted slots : Nat .
651 (lambda unrestricted system : (family IndependentStateSystem slots) .
652 (lambda unrestricted owner : Nat .
653 (lambda unrestricted resume : Nat .
654 (lambda unrestricted epoch : Nat .
655 (lambda unrestricted steps : Nat .
656 (naturalAnd
657 (niOwnersAdmitted slots system)
658 (naturalAnd
659 (naturalLess owner (niOwners slots system))
660 (naturalAnd
661 (naturalLessOrEqual resume 1)
662 (naturalAnd
663 (naturalNonzero epoch)
664 (naturalAnd
665 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
666 (naturalBelowTwoPower 64 steps))))))))))))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.