Statements in Presberger arithmetic are equivalent to systems of linear equations/inequalities, which are representable as matrices. That's why both provers and this exponentiation scheme work. If you have two variables multiplied together, you're beyond Presberger arithmetic and linear equations. The simple matrix representation no longer applies.