Completion settings:
Axiom: aa=b.
Flip LHS and RHS.
Defines rule #2.
Referenced by [2].
Axiom: ac=b.
Reduce RHS:
Defines rule #1.