Is my skolem normal form of $(\forall x \exists y \exists z T(x,y)\land S(y,z))\land (\lnot \forall yP(y))$ correct?
$$ \begin{array}{|c|c|} \hline ( \forall x \exists y \exists z \; T(x,y) \land S(y,z) ) \land (\neg \forall y \; P(y)) & \leftarrow\text{Given formula} \\ \hline ( \forall x \exists y \exists z \; T(x,y) \land S(y,z)) \land (\neg \forall y \; P(y)) & \text{Rename variables and} \\ {} & \text{change quantors} \\ \hline ( \forall x \exists y \exists z \; (T(x,y) \land S(y,z)) ) \land (\exists v \; \neg P(v)) & \text{Remove $()$ and move} \\ {} & \text{$\exists v$ to the left side} \\ \hline \forall x \exists y \exists z \exists u \; T(x,y) \land S(y,z) \land \neg P(u) & \text{It is in PNF. Do:} \\ {} & \exists y = i(x); \exists z = k(x); \\ {} & \exists u = h(x) \\ \hline \forall x \; T(x, i(x)) \land Q(f(x), k(x)) \land \neg P(h(x)) & \text{It is in SNF.} \\ \hline \end{array} $$ (Original picture of the calculation here.)
