Certificate for #2173 ⟨a, b | aaababa=bba⟩

Back:⟨a, b | aaababa=bba⟩

Completion settings:

[1] aaababa=bba

Axiom: aaababa=bba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #1.

Referenced by [3], [5].

[3] aaababa=c

Simplify [1] aaababa=bba.

Reduce RHS:

[2](bba)
⇒ c

Defines rule #2.

Referenced by [4], [5].

[4] aaababc=caababa

Overlap of [3] aaababa=c with [3] aaababa=c:

aaabab a aaababa

Critical pair: aaababc=caababa.

Defines rule #4.

[5] bbc=caababa

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

bb a aaababa

Critical pair: bbc=caababa.

Defines rule #3.