the host's side (its schedule, and the AdamW sites the realization
placed), then (only when it holds) the device's: the plan's order, then
(only when it holds) the run's -- a refusal stops at the first that fails
629def coppeliusHostAdmitted =
630 (lambda unrestricted qmdExpanded : Nat .
631 (lambda unrestricted pushExpanded : Nat .
632 (lambda unrestricted realized : (family CoppeliusRealizedTables) .
633 (nat-eliminate (lambda unrestricted host : Nat . Nat) 0
634 (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat .
635 (nat-eliminate (lambda unrestricted plan : Nat . Nat) 0
636 (lambda unrestricted q : Nat . (lambda unrestricted ignoredToo : Nat . (naturalIsZero (coppeliusRunDeviceHazardOf q))))
637 (naturalIsZero (coppeliusDeviceHazardOf p)))))
638 (naturalAnd coppeliusSchedulesAdmitted
639 (naturalAnd (coppeliusHostLearnerAdmitted pushExpanded realized) (coppeliusHostCertified qmdExpanded pushExpanded realized)))))))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.