Certificate for #2504 ⟨a, b | aababa=baab⟩

Back:⟨a, b | aababa=baab⟩

Completion settings:

[1] aababa=baab

Axiom: aababa=baab.

Referenced by [3].

[2] baab=c

Axiom: baab=c.

Defines rule #4.

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

[3] aababa=c

Simplify [1] aababa=baab.

Reduce RHS:

[2](baab)
⇒ c

Defines rule #5.

Referenced by [5], [6].

[4] baac=caab

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

baa b baab

Critical pair: baac=caab.

Defines rule #2.

[5] aabac=cab

Overlap of [3] aababa=c with [2] baab=c:

aaba ba baab

Critical pair: aabac=cab.

Defines rule #3.

[6] bc=caba

Overlap of [2] baab=c with [3] aababa=c:

b aab aababa

Critical pair: bc=caba.

Defines rule #1.