Newbie to induction attempt to find natural deduction proof with given axioms I am trying to prove the conjecture: 
$∀x.∀y.∀z.(x+y)+z=x+(y+z)$
I have access to the following axioms plus induction, and the others regular rules of natural deduction.
$A1: nat(0)$
$A2: nat(T) ⊢ nat(s(T))$
$A3: nat(T), nat(U) ⊢ nat(T+U)$
$A4: nat(T), nat(U) ⊢ nat(T · U)$
$A5: 1=s(0)$
$A6: ∀x. 0+x=x$
$A7: ∀x.∀y.s(x)+y=s(x+y)$
$A8: ∀x.0·x = 0$
$A9: ∀x.∀y.s(x)·y = y + x · y$
I am really close to completing this proof however I am not sure about how to complete it with the brackets issues...:

 A: The trouble you are having is because you never use your inductive hypothesis (line 16).  This is what you need to go through:
$(s(a2) + a3) + a4 = (\text{using} A7: s(a2) + a3 = s(a2 + a3))$
$s(a2 + a3) + a4 = (\text{using } A7 \text{ again})$
$s((a2 + a3) + a4) = (\text{use inductive hypothesis! }(a2 + a3) + a4 = a2 + (a3 + a4))$
$s(a2 + (a3 + a4)) =(\text{using } A7)$
$s(a2) + (a3 + a4)$
Below is a formal proof using the computer program called Fitch (which comes with the book Language Proof and Logic):

Please note how the formal proof closely mirrors the mathematical algebraic proof as shown at the beginning of this post: for every mathematical step, I do two steps in the formal proof, a $\forall \: Elim$ followed by a $= \: Elim$. I also start with a 'LHS=LHS' (LHS: left-hand side) statement at the start using a $= \: Intro$ to get the gradual transformation started.  I know you do all these steps at some point as well in your proof, but the order in which you do them seem a bit less organized, so I encourage you to follow the systematic transformation as I do in my proof, because otherwise it is very easy to get lost in all the symbol strings, as I am sure you have noticed!
OK, I got the darn thing ... what a hellish interface!

A: It doesn't follow. [Or didn't before "and induction!"]
Take the model for Robinson Arithmetic and hence your arithmetic at p. 69 of my Gödel book -- and you will see that in that model, with $a$ and $b$ as defined, $(a + b) + a \neq a + (b + a)$.
The basic point is that, since you have no induction axiom inside your arithmetic, you can prove almost none of even the simplest general truths of arithmetic.
I'm being a bit terse, as I have already answered a similar question from the OP -- I'm not sure what book/set of lecture notes is being used here, but something is going awry.
