Certificate for #5233 ⟨a, b | aabbaba=baba⟩

Back:⟨a, b | aabbaba=baba⟩

Completion settings:

[1] aabbaba=baba

Axiom: aabbaba=baba.

Referenced by [3].

[2] baba=c

Axiom: baba=c.

Defines rule #3.

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

[3] aabbaba=c

Simplify [1] aabbaba=baba.

Reduce RHS:

[2](baba)
⇒ c

Referenced by [4].

[4] aabc=c

Overlap of [3] aabbaba=c with [2] baba=c:

aab baba baba

Critical pair: aabc=c.

Defines rule #2.

Referenced by [6].

[5] bac=cba

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

ba ba baba

Critical pair: bac=cba.

Defines rule #1.

[6] babc=cabc

Overlap of [2] baba=c with [4] aabc=c:

bab a aabc

Critical pair: babc=cabc.

Defines rule #4.