Certificate for #4794 ⟨a, b | abaababa=abb⟩

Back:⟨a, b | abaababa=abb⟩

Completion settings:

[1] abaababa=abb

Axiom: abaababa=abb.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

Referenced by [3], [4].

[3] abaababa=cb

Simplify [1] abaababa=abb.

Reduce RHS:

[2](ab)b
⇒ cb

Referenced by [4].

[4] cb=cacca

Overlap of [3] abaababa=cb with [2] ab=c:

abaababa ab

Critical pair: caababa=cb.

Reduce LHS:

[2]ca(ab)aba
[2]⇒ cac(ab)a
⇒ cacca

Flip LHS and RHS.

Defines rule #2.