Certificate for #5199 ⟨a, b | aababba=baaa⟩

Back:⟨a, b | aababba=baaa⟩

Completion settings:

[1] aababba=baaa

Axiom: aababba=baaa.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #1.

Referenced by [3], [4].

[3] aababba=caa

Simplify [1] aababba=baaa.

Reduce RHS:

[2](ba)aa
⇒ caa

Referenced by [4].

[4] caa=aacbc

Overlap of [3] aababba=caa with [2] ba=c:

aa babba ba

Critical pair: aacbba=caa.

Reduce LHS:

[2]aacb(ba)
⇒ aacbc

Flip LHS and RHS.

Defines rule #2.