Power-like maps in n-abelian semigroups

We employ automated deduction techniques to prove and generalize some well-known theorems in group theory that involve power maps, i.e., functions of the form f(x)=xn. The main difficulty is that if n is interpreted as an integer variable, then the results are not expressible in first-order logic of groups or semigroups, and hence not provable by modern first-order theorem provers. Here we demonstrate that an appropriate reformulation of power maps makes some basic mathematical concepts like GCD and mathematical induction accessible to the first-order automated theorem proving, allowing even for generalizations of the classical commutativity theorems in (semi)group theory.