I read:
I don't think the first step is necessary. Can anyone prove or disprove providing a counterexample that we reach non-equivalent predicate formulas?
Kind of formulas I'm talking about are: $$\exists u((\exists x(A(x)\implies\forall y B(x,y)))\implies(\exists zC(z)\implies\forall B(u,w)))$$ or: $$((\exists x_1A(x_1)\wedge\exists x_2B(x_2))\implies\exists x_3C(x_3))\implies \exists x_4D(x_4)$$
Step 1 should be written explicitly as convert all sub expressions of the form $A \iff B$ into $A \implies B \land B \implies A$, and then convert all sub expressions of the form $A \implies B$ into $\lnot A \lor B$.
If you skip step (1), then step (4) won't work. This is because, for example:
$$\begin{array} {rl} % (\forall x~A(x)) \implies B &= \lnot(\forall x~A(x)) \lor B \\ % &= (\exists x~ \lnot A(x)) \lor B \\ % &= \exists x~ (\lnot A(x) \lor B) \\ % &= \exists x~ (A(x) \implies B) \\ % \end{array}$$
The point is that it is not always the case that $(\forall x~A(x)) \implies B$ is logically equivalent to $\forall x~(A(x) \implies B)$. So a counter example would be any instance of $$(\forall x~A(x)) \implies B$$ where $\exists x~ (A(x) \implies B)$ isn't equivalent to $\forall x~ (A(x) \implies B)$. So for counter example, $A(x)$ is $x=1$ and $B$ is $1=1$.
So you can't just move quantifiers to the front of a formula unless all $\lnot$s are all on the leaves, and the only other boolean operators present are $\lor$ and $\land$.
Aside, hopefully your text mentions somewhere that this algorithm only works in a nonempty universe, since
$$A \land \forall x ~ B(x) = \forall x ~ A \land B(x)$$
doesn't hold when $A$ is false and the universe is empty. This post should help explain the reasoning behind the above algorithm.
You don't have to eliminate implications or move negations in, but the rule for moving the quantifiers out needs to take them into account: to do this you use the following equivalences $$ \begin{array}{rcl} (\exists x(A(x)) \to B &\equiv& \forall x(A(x) \to B)\\ (\forall x(A(x)) \to B &\equiv& \exists x(A(x) \to B)\\ A \to (\exists x(B(x)) &\equiv& \exists x (A \to B(x))\\ A \to (\forall x(B(x)) &\equiv& \forall x (A \to B(x))\\ \lnot(\exists x(A(x))) &\equiv& \forall x (\lnot(A(x)))\\ \lnot(\forall x(A(x))) &\equiv& \exists x (\lnot(A(x)))\\ \end{array} $$ (with bound variables renamed as necessary to avoid variable capture). What is happening here is that existential quantifiers in negative positions (left-hand operand of $\to$, operand of $\lnot$) become universal when you move them out and vice versa when you move universal quantifiers out. In positive positions (right-hand operand of $\to$, either operand of $\lor$ or $\land$) the quantifiers stay the same when you pull them out.
You have to expand $A \leftrightarrow B$ into $(A \to B) \land (B \to A)$, because $A$ and $B$ appear both positively and negatively in $A \leftrightarrow B$.
