         pre-1      (:pre G-1)]
     (doseq [v base-set-1,
             r R,
-            :when (seq (.get remove [v r]))] ;i.e. (not (empty? (.get remove [v r])))
+            :when (not-empty (.get remove [v r]))]
       (.add non-empty-removes [v r]))
     (while-let [[v r] (first non-empty-removes)]
       (doseq [w (.get remove [v r]),

  term. New definitions go into the atom new-names."
  [term goal new-names]
  (cond
   (goal term) term
   (tbox-target-pair? term) (let [[tbox target] (expression-term term),
                                  [tbox-map trans] (uniquify-tbox-map (tbox->hash-map tbox))]
                              (add-names new-names tbox-map)
                              (trans (make-dl-expression (expression-language term) target)))
   :else (let [new-sym (make-dl-expression (expression-language term) (gensym))]
           (add-name new-names new-sym (conjunctors term))
           new-sym)))

(defn- normalize-term
  "Normalizes conjunctor term. New definitions go into the atom new-names."

        (.put remove [v r]
              (set-of w [w base-set-2,
                         :let [post-w (post-2 w r)]
                         :when (not-empty post-w)
                         :let [sim-v (.get sim v)]
                         :when (forall [x post-w] (not (contains? sim-v x)))]))))
    (doseq [w base-set-2]
