844def dpotRunAdmitted =
845 (lambda unrestricted c : Nat .
846 (lambda unrestricted u : Nat .
847 (lambda unrestricted system : (family DataParallelSystem c u) .
848 (lambda unrestricted q : Nat .
849 (lambda unrestricted p : Nat .
850 (lambda unrestricted g : Nat .
851 (lambda unrestricted fanout : Nat .
852 (lambda unrestricted role : Nat .
853 (lambda unrestricted addresses : (family StdList Bytes) .
854 (lambda unrestricted resume : Nat .
855 (lambda unrestricted epoch : Nat .
856 (lambda unrestricted steps : Nat .
857 (naturalAnd
858 (dataParallelAdmitted c u system)
859 (naturalAnd
860 (nativePeerTreeListedAdmitted
861 fanout
862 (dpOwners c u system)
863 role
864 addresses)
865 (naturalAnd
866 (naturalLessOrEqual resume 1)
867 (naturalAnd
868 (naturalNonzero epoch)
869 (naturalAnd
870 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
871 (naturalAnd
872 (naturalNonzero steps)
873 (naturalAnd
874 (naturalBelowTwoPower 64 steps)
875 (naturalAnd
876 (naturalAnd
877 (naturalLessOrEqual p 1)
878 (naturalLessOrEqual g 1))
879 (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.