2476def dpoRunAdmitted =
2477 (lambda unrestricted c : Nat .
2478 (lambda unrestricted u : Nat .
2479 (lambda unrestricted system : (family DataParallelSystem c u) .
2480 (lambda unrestricted q : Nat .
2481 (lambda unrestricted p : Nat .
2482 (lambda unrestricted g : Nat .
2483 (lambda unrestricted role : Nat .
2484 (lambda unrestricted addresses : (family StdList Bytes) .
2485 (lambda unrestricted resume : Nat .
2486 (lambda unrestricted epoch : Nat .
2487 (lambda unrestricted steps : Nat .
2488 (naturalAnd
2489 (dpRunAdmitted c u system role addresses resume epoch steps)
2490 (naturalAnd
2491 (naturalAnd (naturalLessOrEqual p 1) (naturalLessOrEqual g 1))
2492 (dataParallelSeparable c u system q))))))))))))))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.