Certificate for #4478 ⟨a, b | aaba=b, aaaaa=1⟩

Back:⟨a, b | aaba=b, aaaaa=1⟩

Completion settings:

[1] aaba=b

Axiom: aaba=b.

Referenced by [3], [4].

[2] aaaaa=1

Axiom: aaaaa=1.

Defines rule #1.

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

[3] aab=baaaa

Overlap of [1] aaba=b with [2] aaaaa=1:

aab a aaaaa

Critical pair: aab=baaaa.

Referenced by [4].

[4] abaaaa=ba

Overlap of [2] aaaaa=1 with [1] aaba=b:

aaa aa aaba

Critical pair: aaab=ba.

Reduce LHS:

[3]a(aab)
⇒ abaaaa

Referenced by [5].

[5] ab=baa

Overlap of [4] abaaaa=ba with [2] aaaaa=1:

ab aaaa aaaaa

Critical pair: ab=baa.

Defines rule #2.