468def nitRunAdmitted =
469 (lambda unrestricted slots : Nat .
470 (lambda unrestricted system : (family IndependentStateSystem slots) .
471 (lambda unrestricted fanout : Nat .
472 (lambda unrestricted role : Nat .
473 (lambda unrestricted addresses : (family StdList Bytes) .
474 (lambda unrestricted resume : Nat .
475 (lambda unrestricted epoch : Nat .
476 (lambda unrestricted steps : Nat .
477 (naturalAnd
478 (niOwnersAdmitted slots system)
479 (naturalAnd
480 (nativePeerTreeListedAdmitted fanout (niOwners slots system) role addresses)
481 (naturalAnd
482 (naturalLessOrEqual resume 1)
483 (naturalAnd
484 (naturalNonzero epoch)
485 (naturalAnd
486 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
487 (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.