Find a predicate form in prenex normal form which is logically equivalent to using the equivalences:

(a)$\displaystyle ((Agxy \vee Bz) \to \exists y (By \to Bgy))$

(b)$\displaystyle (\forall x (Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

Attempt:

(a)$\displaystyle ((Agxy \vee Bz) \to \exists y (By \to Bgy))$

Here we only have one quantifier to be shifted to the front, so we can use equivalence number 12 to get

$\displaystyle \exists y ((Agxy \vee Bz) \to (By \to Bgy))$

Is this right? Because we are only justified in using this equivalence if the variable y doesn not occur free in $\displaystyle (Agxy \vee Bz)$, but we don't know that since y doesn't not appear in the scope of any quantifiers in it...

(b)$\displaystyle (\forall x(Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

$\displaystyle \forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

In our case the variables are not distinct so we can't apply the equivalcences straight away, so we have to change bound variables first so that we can move quantifiers past the free variables:

$\displaystyle \forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))$

Now, I'm a bit confused about the negation, but I applied equivalence number 4

$\displaystyle \forall x \neg \exists z ((Cxyz \to Bx) \wedge \forall w (Dzy \to Dwy))$

Now we apply equivalence number 3

$\displaystyle \forall x \neg \exists z \forall w((Cxyz \to Bx) \wedge (Dzy \to Dwy))$

I would appreciate it if anyone could correct me.