Certificate for #2259 ⟨a, b | aabbaab=bba⟩

Back:⟨a, b | aabbaab=bba⟩

Completion settings:

[1] aabbaab=bba

Axiom: aabbaab=bba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #1.

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

[3] aabbaab=c

Simplify [1] aabbaab=bba.

Reduce RHS:

[2](bba)
⇒ c

Referenced by [4].

[4] aacab=c

Overlap of [3] aabbaab=c with [2] bba=c:

aa bbaab bba

Critical pair: aacab=c.

Defines rule #2.

Referenced by [5], [6].

[5] bbc=cacab

Overlap of [2] bba=c with [4] aacab=c:

bb a aacab

Critical pair: bbc=cacab.

Defines rule #4.

[6] aacac=cba

Overlap of [4] aacab=c with [2] bba=c:

aaca b bba

Critical pair: aacac=cba.

Defines rule #3.