Definition 1 Let $A$ be any wf. of a first order language L and $x$ be any variable. We say $x$ occurs free in $A$ if there is at least one occurrence of $x$ in $A$ which is not the scope of $(\forall x)$.
Definition 2 Let $A$ be any wf. of a first order language L. A term $t$ is free for $x$ in $A$, if $x$ does not occur free in $A$ within the scope of a $(\forall y)$, where $y$ is any variable occurring in $t$.
I feel quite confused about the second definition. I was wondering if there's no $(\forall y)$ occurring in $A$, then how does the definition work?
In the textbook, there's an example, say, "the term $f_1^2(x_1,x_3)$ is free for $x_1$ in $(\forall x_2)A_1^2(x_1,x_2)\Rightarrow A_1^1(x_1)$ but is not free for $x_1$ in $(\forall x_3)(\forall x_2)A_1^2(x_1,x_2)\Rightarrow A_1^1(x_1).$"
For the first part, there is no $(\forall x_1)$ or $(\forall x_3)$ occurring in the wf. $(\forall x_2)A_1^2(x_1,x_2)\Rightarrow A_1^1(x_1)$. (Here $x_1$ occurs free in the wf.) So, for the definition, if there's no $(\forall y)$ in the wf. $A$, where $y$ is any variable occurring in $t$, then "$t$ is free for $x$ in $A$" automatically true? But this rule does not work for the second part of the example.
I can understand that the results of this example are reasonable, since the aim of the second definition is that $t$ may be substituted for every free occurrence of $x$ in $A$ without introducing any interactions with quantifiers in $A$. But I am really confused about how to use this definition.
Could you help me clarify this definition? Thank you so much!