Certificate for #2330 ⟨a, b | abababa=aab⟩

Back:⟨a, b | abababa=aab⟩

Completion settings:

[1] abababa=aab

Axiom: abababa=aab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

Referenced by [3], [4].

[3] abababa=ac

Simplify [1] abababa=aab.

Reduce RHS:

[2]a(ab)
⇒ ac

Referenced by [4].

[4] ac=ccca

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

abababa ab

Critical pair: cababa=ac.

Reduce LHS:

[2]c(ab)aba
[2]⇒ cc(ab)a
⇒ ccca

Flip LHS and RHS.

Defines rule #2.