    :Arguments
    :Argument])
 
-(def nonterms-exclude-simplify #{:Negation :QuantifierNegation})
+(def nonterms-exclude-simplify
+  "These nonterms will not be simplified."
+  #{:Negation :QuantifierNegation})
+
+(defn- -reconstruct-node
+  "Reconstructs node from nonterm key and children."
+  [key children]
+  (into [key] children))
 
 (defn- -simplify-tree-by
-  [key]
   "Simplifies hiccup format of instaparse parser tree for specified nonterm.
   This is done by removing superfluous levels of nesting from recursive
   elements. For example, [:Disjunction [:Conjunction [:Implication [:Term]]]]
   becomes just [:Term]."
+  [key]
   (fn [& children]
     (if (and (not (contains? nonterms-exclude-simplify key))
              (= (count children) 1))
       ;; Return the only child.
       (first children)
       ;; Don't change anything here.
-      (into [key] children))))
+      (-reconstruct-node key children))))
+
+(defn nonterm?
+   "Tests if node is a nonterminal."
+  ([node]
+   (and (vector? node) (keyword? (first node))))
+  ([node & nonterm-contents]
+     (and (nonterm? node)
+          ;; Only compare first N children, where N is number of additional
+          ;; args specified.
+          (= nonterm-contents (take (count nonterm-contents) node)))))
 
 (defn simplify-tree
+  "Applies -simplify-tree-by for all nonterms (except excluded)."
   [tree]
   (insta/transform
     ;; This makes a map of :NonTerminal -> simplify-tree-by-:NonTerminal.


(defn- -negate-quantifier
  [quantifier]
  (if (= (first quantifier) :QuantifierNegation)
    (second quantifier)
    [:QuantifierNegation quantifier]))

(defn- -negate-formula
  [formula]
  (if (= (first formula) :QuantifiedFormula)
    (let [[_ quantifier formula] formula]
      ;; This will, in turn, negate the formula in next iteration.
      [:QuantifiedFormula (-negate-quantifier quantifier) formula])

      :Conjunction [:Disjunction (-negate-formula lhs) (-negate-formula rhs)]
      :Disjunction [:Conjunction (-negate-formula lhs) (-negate-formula rhs)]
      :Negation lhs
      ;; This is a custom rule, used for ~(\\A x) forms. Replace it with form
      ;; that can be negated in next run with the other rule.
      :QuantifiedFormula [:QuantifiedFormula (-negate-quantifier lhs) rhs]
      ;; In default case, do nothing - reconstruct original node.
      (-reconstruct-node :Negation children))))

(defn- -transform-quantifier-negation
  [& children]
  (let [[quantifier formula] children]
    (if (nonterm? quantifier :QuantifierNegation)
      (let [[[_ foreach-exists literal]] (rest quantifier)]
        (-reconstruct-node :QuantifiedFormula
                           [[:Quantifier
