Certificate for #1836 ⟨a, b | aaaaabaa=ba⟩

Back:⟨a, b | aaaaabaa=ba⟩

Completion settings:

[1] aaaaabaa=ba

Axiom: aaaaabaa=ba.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #4.

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

[3] aaaaabaa=c

Simplify [1] aaaaabaa=ba.

Reduce RHS:

[2](ba)
⇒ c

Referenced by [4].

[4] aaaaaca=c

Overlap of [3] aaaaabaa=c with [2] ba=c:

aaaaa baa ba

Critical pair: aaaaaca=c.

Defines rule #2.

Referenced by [5], [6].

[5] bc=caaaaca

Overlap of [2] ba=c with [4] aaaaaca=c:

b a aaaaaca

Critical pair: bc=caaaaca.

Defines rule #3.

[6] aaaaacc=caaaaca

Overlap of [4] aaaaaca=c with [4] aaaaaca=c:

aaaaac a aaaaaca

Critical pair: aaaaacc=caaaaca.

Defines rule #1.