Certificate for #5232 ⟨a, b | aabbaba=baab⟩

Back:⟨a, b | aabbaba=baab⟩

Completion settings:

[1] aabbaba=baab

Axiom: aabbaba=baab.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #1.

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

[3] aabbaba=cab

Simplify [1] aabbaba=baab.

Reduce RHS:

[2](ba)ab
⇒ cab

Referenced by [4].

[4] aabcc=cab

Overlap of [3] aabbaba=cab with [2] ba=c:

aab baba ba

Critical pair: aabcba=cab.

Reduce LHS:

[2]aabc(ba)
⇒ aabcc

Defines rule #2.

Referenced by [5].

[5] bcab=cabcc

Overlap of [2] ba=c with [4] aabcc=cab:

b a aabcc

Critical pair: bcab=cabcc.

Defines rule #4.

Referenced by [6].

[6] bcac=cabcca

Overlap of [5] bcab=cabcc with [2] ba=c:

bca b ba

Critical pair: bcac=cabcca.

Defines rule #3.