Every diassociative \(A\)-loop is Moufang (Q2759004)

Given a loop \((L,\cdot)\), for any \(x\in L\) let \(L(x)\) and \(R(x)\) be the left and the right translation by \(x\), let \(\text{Mlt}(L):=\langle L(x),R(x)\mid x\in L\rangle\) be the subgroup of \(\text{Sym }L\) generated by all left and right translations and let \(\text{Mlt}_1(L):=\{\phi\in\text{Mlt}(L)\mid\phi(1)=1\}\). \(\text{Mlt}_1(L)\) is called the inner mapping group of the loop \((L,\cdot)\) and, in the associative case, it is the group of inner automorphisms of \((L,\cdot)\). A loop \((L,\cdot)\) is called an \(A\)-loop if \(\text{Mlt}_1(L)\leq\Aut(L,\cdot)\). Every \(A\)-looop is always power associative (i.e. every \(\langle x\rangle\) is a group) but not necessarily diassociative (i.e. every \(\langle x,y\rangle\) is a group). On the other hand, if \((L,\cdot)\) is a Moufang loop (i.e. \(\forall x,y,z\in L\), \(x(y(xz))=((xy)x)z\)) then it is diassociative. In this note the authors shed light on the relationship between Moufang loops and \(A\)-loops, showing that every diassociative \(A\)-loop is a Moufang loop. They resort to computer-aided proofs via McCune's OTTER program, also commenting on some drawbacks thereof, and the need of ``humanization'' of counterintuitive procedures.