Does anybody understand this?...



Given the following term signature:
Code:
sorts    NAT
ops      zero:	NAT
         succ:	NAT->NAT

+ops     plus:	NAT,NAT->NAT
+defns   (x, y: NAT)
         plus(zero, x) = x
         plus(succ(y), x) = succ(plus(y, x)
Prove that the quotient term structure is associative,

ie. plus(plus(x, y), z) = plus(x, plus(y, z)) for all terms x, y, z.


I am having a lot of trouble with this proof by induction business. Has anyone come across it before?



[Edited by HarryW on 11-05-2000 at 10:30 PM]