Do the Moufang identities *themselves* imply diassociativity / Moufang's theorem / Artin's theorem? A Moufang loop is a loop satisfying the Moufang identities.  Famously, these are diassociative -- the subloop generated by any two elements is associative (is a group) -- and more generally, they satisfy Moufang's theorem, that if any three elements associate, then so do anything they generate (i.e. they generate a group).
Separately, if you have an alternative algebra or ring, then multiplication in it also satisfies the Moufang identities, is also diassociative, and also satisfies the analogue of Moufang's theorem.
Now, in the case where every nonzero element has an inverse (as in the octonions), you could prove the latter by just appealing to Moufang's theorem for loops.  But in general you can't do that.
So, something is going on here -- the Moufang identities, together with inverses, imply Moufang's theorem; and the Moufang identities, together with the existence of an addition operation that our multiplication distributes over, implies Moufang's theorem.
It seems really funny to me that in both these cases, these identities imply the same result, but in each case, we need a different auxiliary assumption to make it work.
So: Do the Moufang identities themselves imply Moufang's theorem?  That is to say, if we have a magma (and let's say it has an identity because we may as well), and it satisfies the Moufang identities, does it automatically satisfy the analogue of Moufang's theorem, including being diassocative?  Or is there some counterexample to this?
(And if the theorem doesn't hold in this setting, is there some simple additional assumption we could make, that would make it true, while also covering both the cases above?)
I'm really wondering about this because this seems like an obvious question to ask, whether we can unify these two settings, but I haven't seen an answer stated anywhere.
Thank you all!
 A: OK, I have an answer to my question: No, the identities alone are not enough, not even to prove diassociativity.  More specifically, they're not sufficient to prove $(xy)(xy)$ equal to any of the other parenthesizations of $xyxy$ (although the others are all equal).
Basically, they don't prove that, because, well, we can just try applying them in all possible ways, and see that they don't.  To make this more formal, and combinatorial rather than proof-theoretic, we can construct the free unital magma that's subject to these relations.  That is to say, elements will either be the identity $e$, or will be [equivalence classes of] of binary trees whose leaves each labeled with $a$ or $b$.  Multiplication is joining trees (or doing nothing if you multiply by the identity).  Equivalence of trees is given by the alternative, flexible, and Moufang identities, these representing transformations that we can apply to subtrees (hence why I separate out alternative/flexible from Moufang despite them following from them in the presence of a unit; I want to describe things in terms of what we do to trees).
Importantly, none of these transformations change the size of anything, so all equivalence classes are finite, and if you start with one representative, you can exhaustively explore the whole class and see what's in it.
Then, well, there are simply no valid transformations to apply to $(ab)(ab)$; it's in an equivalence class by itself.  Alternative and flexible identities don't apply because breaking this down into a multiplication of three (non-identity) things, those three things are always $a$, $b$, and $ab$; no two of them are equal.  Moufang identities don't apply because the factors would have to be the individual leaves, and none of them work there.
So, the Moufang identities truly are not enough by themselves.
That said, they do seem to apply power-associativity by themselves (in the presence of a unit).  Basically if we assume that $x^m$ is well-defined for $m<n$, and we have $x^kx^\ell$ with $k+\ell=n$, if $k,\ell>1$ we can write this as $(xx^{k-1})(x^{\ell-1} x)$ and conclude by the inductive hypothesis that this is equal to $xx^{n-1}$.  So that's neat.
...I kind of don't want to "accept" this answer, as I'm still really wondering if there is any way to unify the two different settings where they do imply diassociativity and [an analogue of] Moufang's theorem.  If anyone has an answer to that, I'd love to hear it!
