Certificate for #4300 ⟨a, b | ababababa=ab⟩

Back:⟨a, b | ababababa=ab⟩

Completion settings:

[1] ababababa=ab

Axiom: ababababa=ab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #2.

Referenced by [3], [4], [5].

[3] ababababa=c

Simplify [1] ababababa=ab.

Reduce RHS:

[2](ab)
⇒ c

Referenced by [4].

[4] cccca=c

Overlap of [3] ababababa=c with [2] ab=c:

ababababa ab

Critical pair: cabababa=c.

Reduce LHS:

[2]c(ab)ababa
[2]⇒ cc(ab)aba
[2]⇒ ccc(ab)a
⇒ cccca

Defines rule #1.

Referenced by [5].

[5] cb=ccccc

Overlap of [4] cccca=c with [2] ab=c:

cccc a ab

Critical pair: ccccc=cb.

Flip LHS and RHS.

Defines rule #3.