Certificate for #5663 ⟨a, b | aabaab=baaba⟩

Back:⟨a, b | aabaab=baaba⟩

Completion settings:

[1] aabaab=baaba

Axiom: aabaab=baaba.

Referenced by [3].

[2] baaba=c

Axiom: baaba=c.

Defines rule #3.

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

[3] aabaab=c

Simplify [1] aabaab=baaba.

Reduce RHS:

[2](baaba)
⇒ c

Defines rule #4.

Referenced by [4], [5].

[4] aac=ca

Overlap of [3] aabaab=c with [2] baaba=c:

aa baab baaba

Critical pair: aac=ca.

Defines rule #1.

[5] bc=cab

Overlap of [2] baaba=c with [3] aabaab=c:

b aaba aabaab

Critical pair: bc=cab.

Defines rule #2.