Давайте пошагово рассмотрим на примере вашей формулы:
(1) Имеем
![$\Big(\forall x \big((\exists y \, P(y)) \to Q(x)\big) \Big)\wedge (\forall x \exists y \, R(x,y))$ $\Big(\forall x \big((\exists y \, P(y)) \to Q(x)\big) \Big)\wedge (\forall x \exists y \, R(x,y))$](https://dxdy-04.korotkov.co.uk/f/f/0/7/f07f0b41f4a9a9d07f4d00ee86d8c98682.png)
(2) Формула приводится к н. ф. "снизу-вверх", то есть начиная с самых глубоких подформул, вы так и сделали. Имеем
![$(\exists y \, P(y)) \to Q(x) \sim \forall y (P(y) \to Q(x))$ $(\exists y \, P(y)) \to Q(x) \sim \forall y (P(y) \to Q(x))$](https://dxdy-03.korotkov.co.uk/f/e/6/b/e6be0472345465f37e6217cffd888cdd82.png)
, переменную можно не переименовывать, так как
![$y$ $y$](https://dxdy-02.korotkov.co.uk/f/d/e/c/deceeaf6940a8c7a5a02373728002b0f82.png)
всё одно не входит свободно в
![$Q(x)$ $Q(x)$](https://dxdy-01.korotkov.co.uk/f/8/a/9/8a9e90a4d3d59b0dfcec4f4b5279584282.png)
:
![$\Big(\forall x \forall y (P(y) \to Q(x)) \Big)\wedge (\forall x \exists y \, R(x,y))$ $\Big(\forall x \forall y (P(y) \to Q(x)) \Big)\wedge (\forall x \exists y \, R(x,y))$](https://dxdy-01.korotkov.co.uk/f/c/4/e/c4e5eb9d0e412c52263f0ca488fcfb1c82.png)
.
(3) Теперь из левого конъюнкта выносим
![$\forall x$ $\forall x$](https://dxdy-04.korotkov.co.uk/f/3/5/c/35cb88e174fb5199c8bb8dd4ab84267682.png)
, во второй конъюнкт
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
вободно не входит, поэтому можно не переименовывать:
![$\forall x \Big(\big(\forall y (P(y) \to Q(x)) \big)\wedge (\forall x \exists y \, R(x,y))\Big)$ $\forall x \Big(\big(\forall y (P(y) \to Q(x)) \big)\wedge (\forall x \exists y \, R(x,y))\Big)$](https://dxdy-01.korotkov.co.uk/f/8/e/7/8e78f7e4c40f478e99aa344757342ba182.png)
.
(4) Выносим из первого конъюнкта
![$\forall y$ $\forall y$](https://dxdy-04.korotkov.co.uk/f/f/a/0/fa0cc457b7b4f94c3ce50cf392e01b9682.png)
:
![$\forall x \forall y \Big((P(y) \to Q(x))\wedge (\forall x \exists y \, R(x,y))\Big)$ $\forall x \forall y \Big((P(y) \to Q(x))\wedge (\forall x \exists y \, R(x,y))\Big)$](https://dxdy-02.korotkov.co.uk/f/5/1/c/51cb3742b114d03197d2d9c7df83ee7d82.png)
.
(5) Теперь из второго конъюнкта выносим
![$\forall x$ $\forall x$](https://dxdy-04.korotkov.co.uk/f/3/5/c/35cb88e174fb5199c8bb8dd4ab84267682.png)
, так как
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
теперь входит свободно в первый конъюнкт, то
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
переименуем в
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
:
![$\forall x \forall y \forall z\Big((P(y) \to Q(x))\wedge (\exists y \, R(z,y))\Big)$ $\forall x \forall y \forall z\Big((P(y) \to Q(x))\wedge (\exists y \, R(z,y))\Big)$](https://dxdy-03.korotkov.co.uk/f/e/b/c/ebc0b390e69783f015f9b4eee489f94182.png)
.
(6) Далее выносим
![$\exists y$ $\exists y$](https://dxdy-03.korotkov.co.uk/f/a/c/f/acff59eed7bde02133a7e99a849b845182.png)
, по аналогичным причинам переименовываем:
![$\forall x \forall y \forall z \exists w \Big((P(y) \to Q(x)) \wedge R(z,w)\Big)$ $\forall x \forall y \forall z \exists w \Big((P(y) \to Q(x)) \wedge R(z,w)\Big)$](https://dxdy-03.korotkov.co.uk/f/2/3/c/23c65de338d9a8f5eed3a612e42ba04882.png)
.
Кто-то быть может скажет, что один квантор можно было сэкономить, но это не принципиально.