Certificate for #16544 ⟨a, b | aba=ba, baa=aba⟩

Back:⟨a, b | aba=ba, baa=aba⟩

Completion settings:

[1] aba=ba

Axiom: aba=ba.

Referenced by [2], [4].

[2] baa=ba

Axiom: baa=aba.

Reduce RHS:

[1](aba)
⇒ ba

Referenced by [6].

[3] ba=c

Axiom: ba=c.

Defines rule #3.

Referenced by [4], [5], [6], [7], [8].

[4] aba=c

Simplify [1] aba=ba.

Reduce RHS:

[3](ba)
⇒ c

Referenced by [5].

[5] ac=c

Overlap of [4] aba=c with [3] ba=c:

a ba ba

Critical pair: ac=c.

Defines rule #1.

Referenced by [8].

[6] baa=c

Simplify [2] baa=ba.

Reduce RHS:

[3](ba)
⇒ c

Referenced by [7].

[7] ca=c

Overlap of [6] baa=c with [3] ba=c:

baa ba

Critical pair: ca=c.

Defines rule #2.

[8] bc=cc

Overlap of [3] ba=c with [5] ac=c:

b a ac

Critical pair: bc=cc.

Defines rule #4.