Show a Particular Set of Sentences can be Represented with a WFF Problem
Let $A^{*}_{S}$ be the set of sentences consisting of S1, S2, and all sentences of the form
$\phi (0)\rightarrow\forall v_{1}(\phi (v_{1}\rightarrow\phi(Sv_{1}))\rightarrow\forall v_{1}\phi (v_{1})$
where $\phi$ is a formula ( in the language of $\mathfrak{N}_{S}$ in which no variable except $v_{1}$ occurs free. Show that $A_{S}\subseteq\mathrm{Cn}A^{*}_{S}$. Conclude that $\mathrm{Cn}A^{*}_{S}=\mathrm{Th}\mathfrak{N}_{S}$. (Here $\phi(t)$ is by definition $\phi^{v_{1}}_{t}$. The sentence displayed above is called the induction axiom for $\phi$.)
Where
S1. $\forall x Sx\neq0$
S2. $\forall x \forall y (Sx=Sy\rightarrow x=y)$
S3. $\forall y(y\neq 0 \rightarrow \exists x y=Sx)$
S4.n $\forall x S^nx\neq x$
So Far
So, I understand thus far that to show $A_{S}\subseteq\mathrm{Cn}A^{*}_{S}$ I need to show that the induction axiom above defines S3 and S4.n; I understand that the best way to do this is by induction, and that the base case for showing S3 is (below).  What I do not understand is where to take the induction step from there.
Prove S3
Base Case: Let y in $\forall y(y\neq 0 \rightarrow \exists x y=Sx)$ be 0.  It is the case that $A_{S}^{*}\vdash(0\neq0\rightarrow\exists x0=Sx)$, as the antecedent is logically false ($\vdash 0\ne 0$).
Induction Step: ...Not really sure.
 A: Yes, for $S_3$ you are on the right track.
Your induction formula $\varphi(v_1)$ is :

$(v_1≠0→∃x v_1 = Sx)$,

with only $v_1$ free.
You have already proved the basis case : $\varphi(0)$, i.e. $0≠0→∃x 0 = Sx$.
Now, you have to prove the induction step, i.e.that :

$∀v_1(\varphi(v_1) → \varphi(Sv_1))$.

We have $S(v_1)=S(v_1)$; thus, by $\exists$-introduction :
$\exists x S(v_1)= S(x)$.
Apply now the tautology : $\mathcal A \rightarrow (\mathcal B \rightarrow \mathcal A)$ to get (by modus ponens) :

$Sv_1 \ne 0 \rightarrow \exists x S(v_1)= S(x)$.

Now, by $\forall$-introduction :


$\forall v_1(Sv_1 \ne 0 \rightarrow \exists x S(v_1)= S(x))$.


Finally, having proved $\varphi(0)$ and $∀v_1(\varphi(v_1) → \varphi(Sv_1))$, we may apply the Induction axiom to get :

$\forall v_1 (v_1≠0→∃x v_1 = Sx)$.

Added
Now for $S_{4.n}$, we need a sort of "double induction", on $n$ and on $x$.
Let start with $S_{4.1}$, i.e. $∀xSx≠x$; we will prove it by induction on $x$.
The induction formula is : $\varphi (x) := Sx \ne x$
For $n=0$, we have, by $S_1$ (we instantiate the universal quantifier with $x := 0$), that $S(0) \ne 0$, i.e. $\varphi (0)$.
Assume now as Induction hypotheses that $\varphi (n)$ holds, i.e.that $Sn \ne n$ : we have to show that it holds for $S(n)$. Assume for contradiction that $S(Sn)=Sn$; by $S_2$ we have that : $Sn=n$, contrary to Induction hypotheses; thus $S(Sn) \ne Sn$.
Again, having showed that $\varphi(0)$ and that $\forall x (\varphi(x) \rightarrow \varphi (Sx))$, we conclude that :


$\forall x \varphi(x)$, i.e.


$\forall x Sx \ne x$.
Thus, we have proved $S_{4.1}$; this is the basis for the "outer" induction on the "counter" $k$ of $S_{4.k}$.
We have now to prove that if $S_{4.k}$ holds, then also $S_{4.k+1}$ holds.
