Certificate for #5231 ⟨a, b | aabbaba=baaa⟩

Back:⟨a, b | aabbaba=baaa⟩

Completion settings:

[1] aabbaba=baaa

Axiom: aabbaba=baaa.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #1.

Referenced by [3], [4].

[3] aabbaba=caa

Simplify [1] aabbaba=baaa.

Reduce RHS:

[2](ba)aa
⇒ caa

Referenced by [4].

[4] caa=aabcc

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

aab baba ba

Critical pair: aabcba=caa.

Reduce LHS:

[2]aabc(ba)
⇒ aabcc

Flip LHS and RHS.

Defines rule #2.