Certificate for #884 ⟨a, b | aaaabaa=ba⟩

Back:⟨a, b | aaaabaa=ba⟩

Completion settings:

[1] aaaabaa=ba

Axiom: aaaabaa=ba.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #4.

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

[3] aaaabaa=c

Simplify [1] aaaabaa=ba.

Reduce RHS:

[2](ba)
⇒ c

Referenced by [4].

[4] aaaaca=c

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

aaaa baa ba

Critical pair: aaaaca=c.

Defines rule #2.

Referenced by [5], [6].

[5] bc=caaaca

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

b a aaaaca

Critical pair: bc=caaaca.

Defines rule #3.

[6] aaaacc=caaaca

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

aaaac a aaaaca

Critical pair: aaaacc=caaaca.

Defines rule #1.