Lets say that $\phi$ is written in a Prenexed form, if it is in prenex normal form and there is a formula $\phi^*$ that is not in prenex normal form such that $\phi^*$ is equivalent to $\phi$ and $\phi^*$ results from mere pulling in of some quantifiers in the prefix of $\phi$ to the inside of $\phi$, with or without change of quantifier symbols (i.e.; $\forall$ to $\exists$ or $\exists$ to $\forall$) during that pulling.
For example: $\forall x (\neg \phi)$ ..Pull in $\forall x$ but convert it to $\exists x$ during the pulling to have $ (\neg \exists x \phi)$. Also $\exists x (\phi \to \psi)$ ..Pull in $\exists x$ and turn it into $\forall x $ during the pulling to have $(\forall x \phi \to \psi)$.
Now I want to coin a syntactical notion of pure non-Prenexed form to mean that the formula is not in Prenexed form, nor is any of its subformulas.
Is that notion decidable?