I was given the Language $L=\left \{ a^nb^na^nb^n |n\epsilon \mathbb{N} \right \}$ and I'm supposed to find a Grammar that generates that Language. After some trying and fiddling I found one that I think works. The question is how do I verify it? On paper it looks fine, but are there some tools check this for me? Also are there easier methods than trying out by hand or brute force?
The Grammar I found is as follows:
$S\rightarrow aB_{1}A_{2}B_{2}|aB_{1}PA_{2}B_{2}$
$P\rightarrow A_{1}B_{1}A_{2}B_{2}|A_{1}B_{1}PA_{2}B_{2}$
$B_{1}A_{1}\rightarrow X_{A1}A_{1}$
$X_{A1}A_{1}\rightarrow X_{A1}X_{B1}$
$X_{A1}X_{B1}\rightarrow A_{1}X_{B1}$
$A_{1}X_{B1}\rightarrow A_{1}B_{1}$
$B_{2}A_{2}\rightarrow X_{A2}A_{2}$
$X_{A2}A_{2}\rightarrow X_{A2}X_{B2}$
$X_{A2}X_{B2}\rightarrow A_{2}X_{B2}$
$A_{2}X_{B2}\rightarrow A_{2}B_{2}$
$aA_{1}\rightarrow aa$
$aB_{1}\rightarrow ab$
$bB_{1}\rightarrow bb$
$bA_{2}\rightarrow ba$
$aA_{2}\rightarrow aa$
$aB_{2}\rightarrow ab$
$bB_{2}\rightarrow bb$