Certificate for #1132 ⟨a, b | abbaab=baa⟩

Back:⟨a, b | abbaab=baa⟩

Completion settings:

[1] abbaab=baa

Axiom: abbaab=baa.

Referenced by [3].

[2] baa=c

Axiom: baa=c.

Defines rule #3.

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

[3] abbaab=c

Simplify [1] abbaab=baa.

Reduce RHS:

[2](baa)
⇒ c

Referenced by [4].

[4] abcb=c

Overlap of [3] abbaab=c with [2] baa=c:

ab baab baa

Critical pair: abcb=c.

Defines rule #1.

Referenced by [5], [6].

[5] bac=cbcb

Overlap of [2] baa=c with [4] abcb=c:

ba a abcb

Critical pair: bac=cbcb.

Defines rule #2.

[6] abcc=caa

Overlap of [4] abcb=c with [2] baa=c:

abc b baa

Critical pair: abcc=caa.

Defines rule #4.