A normal-form theorem for monoids and groups with the single relation xy<->yx

The word problem for confluent Thue systems is linear-time and for almost confluent systems it is PSPACE-complete. Here we consider a single length-preserving rule, of the form xy<->yx, whose word problem could turn out to be tractable.
A search for normal forms leads to the conjecture that if x^m y^n <->* x^p y^q then m=p and n=q.

We prove a stronger version of this: in a group G with the single relator xyx^{-1}y^{-1} where x and y are non-commuting , if x^my^{-n} = 1 in G then m=n=0.