Using primitive recursion scheme

Hi!

I have to define the scheme of primitive recursion of this function:

$\displaystyle remove_from_left: \Sigma^{*}\mbox{x}\mathbb{N} \rightarrow \Sigma^{*}$

Some examples:

$\displaystyle removefromleft(abcdc,7)=\epsilon$

$\displaystyle removefromleft(abcdc,3)=dc$

First I gave a inductive definition for $\displaystyle \Sigma^{*}\mbox{x}\mathbb{N}$ then $\displaystyle \Sigma^{*}\mbox{x}\mathbb{N}$ is defined inductively by the next rules:

$\displaystyle

(i) (\epsilon,0)\in\Sigma^{*}\mbox{x}\mathbb(N)$

$\displaystyle (ii) \mbox{ If } (w,0)\in\Sigma^{*}\mbox{x}\mathbb{N} and \mbox{x}\in\Sigma \Rightarrow (xw,0)\Sigma^{*}\mbox{x}\mathbb{N}$

$\displaystyle (iii)\mbox{ If } (w,n) \in \Sigma^{*}\mbox{x}\mathbb{N} \Rightarrow (w, n+1)\in\Sigma^{*}\mbox{x}\mathbb{N}$

After that I defined the scheme of primitive recursion for $\displaystyle \Sigma^{*}\mbox{x}N:$:

$\displaystyle \displaystyle \mathbb{H}$ Be $\displaystyle \Sigma^{*}$ a set and be :

-$\displaystyle f_0 \in \Sigma^{*}$

-$\displaystyle f_1:\Sigma^{*}\mbox{x} \mathbb{N} \mbox{x}\Sigma \mbox{x}\Sigma^{*}\rightarrow \Sigma^{*} $

-$\displaystyle f_2:\Sigma^{*}\mbox{x} \mathbb{N}\mbox{x}\Sigma^{*}\rightarrow \Sigma^{*}$

$\displaystyle \mathbb{T}$ Then exist only one function $\displaystyle removefromleft:\Sigma^{*}\mbox{x}\mathbb{N}\righta rrow\Sigma^{*}$ that:

$\displaystyle (i) removefromleft((\epsilon,0))=f_0=\epsilon$

$\displaystyle (ii) removefromleft((xw,0))=f_1((w,0),x,removefromleft( w,0))= xw$

$\displaystyle (iii) removefromleft((w,n+1))=f_2((w,n)$

$\displaystyle ,removefromleft(w,n))=removefromleft(w,n)$

Is this ok? Perhaps I have to change something...

Thank's!

Sorry for my bad english because I speak spanish(Worried)