Next ≝
    LET Unbound ≝ {Pod ∈ Objects : Pod.Kind = "Pod" ∧ ¬ Bound(Pod)} IN
        IF Unbound = {} THEN
          {}
        ELSE
          CHOOSE Pod ∈ Unbound : ∀ Other ∈ Unbound : Pod.Spec.Priority ≥ Other.Spec.Priority