1254def dpRunAdmitted =
1255 (lambda unrestricted c : Nat .
1256 (lambda unrestricted u : Nat .
1257 (lambda unrestricted system : (family DataParallelSystem c u) .
1258 (lambda unrestricted role : Nat .
1259 (lambda unrestricted addresses : (family StdList Bytes) .
1260 (lambda unrestricted resume : Nat .
1261 (lambda unrestricted epoch : Nat .
1262 (lambda unrestricted steps : Nat .
1263 (naturalAnd
1264 (dataParallelAdmitted c u system)
1265 (naturalAnd
1266 (nativePeerStarAdmitted (dpOwners c u system) role addresses)
1267 (naturalAnd
1268 (naturalLessOrEqual resume 1)
1269 (naturalAnd
1270 (naturalNonzero epoch)
1271 (naturalAnd
1272 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
1273 (naturalAnd (naturalNonzero steps) (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.