Prenex normal form. A predicate logic expression is in
      prenex normal form if (1) all its quantifiers are clustered at
      the left, (2) no quantifier is negated, (3) the scope of each
      quantifier extends to the right end of the expression, (4) no
      two quantifiers use the same variable, (5) every letter used
      by a quantifier is used later in the expression as a bound
      variable. Every predicate logic expression can be cast in
      prenex normal form. 

      Translating English sentences into prenex normal form is
      easier and more natural for most people than using any other
      format. 

      For example, "(x)[Ax  (y)(By  Cy)]" can be restated in
      prenex normal form as "(x)(y)[Ax  (By  Cy)]".