Certificate for #4840 ⟨a, b | ababbaba=aab⟩

Back:⟨a, b | ababbaba=aab⟩

Completion settings:

[1] ababbaba=aab

Axiom: ababbaba=aab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

Referenced by [3], [4].

[3] ababbaba=ac

Simplify [1] ababbaba=aab.

Reduce RHS:

[2]a(ab)
⇒ ac

Referenced by [4].

[4] ac=ccbca

Overlap of [3] ababbaba=ac with [2] ab=c:

ababbaba ab

Critical pair: cabbaba=ac.

Reduce LHS:

[2]c(ab)baba
[2]⇒ ccb(ab)a
⇒ ccbca

Flip LHS and RHS.

Defines rule #2.