Certificate for #3969 ⟨a, b | aaabaabaa=ba⟩

Back:⟨a, b | aaabaabaa=ba⟩

Completion settings:

[1] aaabaabaa=ba

Axiom: aaabaabaa=ba.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #4.

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

[3] aaabaabaa=c

Simplify [1] aaabaabaa=ba.

Reduce RHS:

[2](ba)
⇒ c

Referenced by [4].

[4] aaacaca=c

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

aaa baabaa ba

Critical pair: aaacabaa=c.

Reduce LHS:

[2]aaaca(ba)a
⇒ aaacaca

Defines rule #2.

Referenced by [5], [6].

[5] bc=caacaca

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

b a aaacaca

Critical pair: bc=caacaca.

Defines rule #3.

[6] aaacacc=caacaca

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

aaacac a aaacaca

Critical pair: aaacacc=caacaca.

Defines rule #1.