Certificate for #2503 ⟨a, b | aababa=baaa⟩

Back:⟨a, b | aababa=baaa⟩

Completion settings:

[1] aababa=baaa

Axiom: aababa=baaa.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #1.

Referenced by [3], [4].

[3] aababa=caa

Simplify [1] aababa=baaa.

Reduce RHS:

[2](ba)aa
⇒ caa

Referenced by [4].

[4] caa=aacc

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

aa baba ba

Critical pair: aacba=caa.

Reduce LHS:

[2]aac(ba)
⇒ aacc

Flip LHS and RHS.

Defines rule #2.