Certificate for #1120 ⟨a, b | ababab=baa⟩

Back:⟨a, b | ababab=baa⟩

Completion settings:

[1] ababab=baa

Axiom: ababab=baa.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #1.

Referenced by [3], [4].

[3] ababab=ca

Simplify [1] ababab=baa.

Reduce RHS:

[2](ba)a
⇒ ca

Referenced by [4].

[4] ca=accb

Overlap of [3] ababab=ca with [2] ba=c:

a babab ba

Critical pair: acbab=ca.

Reduce LHS:

[2]ac(ba)b
⇒ accb

Flip LHS and RHS.

Defines rule #2.