Certificate for #1259 ⟨a, b | ababa=abab⟩

Back:⟨a, b | ababa=abab⟩

Completion settings:

[1] ababa=abab

Axiom: ababa=abab.

Referenced by [3].

[2] abab=c

Axiom: abab=c.

Defines rule #3.

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

[3] ababa=c

Simplify [1] ababa=abab.

Reduce RHS:

[2](abab)
⇒ c

Referenced by [4].

[4] ca=c

Overlap of [3] ababa=c with [2] abab=c:

ababa abab

Critical pair: ca=c.

Defines rule #1.

Referenced by [5].

[5] cb=abc

Overlap of [2] abab=c with [2] abab=c:

ab ab abab

Critical pair: abc=cab.

Reduce RHS:

[4](ca)b
⇒ cb

Flip LHS and RHS.

Defines rule #2.