Certificate for #12271 ⟨a, b | aaab=ba, aaba=b⟩

Back:⟨a, b | aaab=ba, aaba=b⟩

Completion settings:

[1] aaab=ba

Axiom: aaab=ba.

Referenced by [3].

[2] aaba=b

Axiom: aaba=b.

Referenced by [3], [4].

[3] ab=baa

Overlap of [1] aaab=ba with [2] aaba=b:

a aab aaba

Critical pair: ab=baa.

Defines rule #2.

Referenced by [4].

[4] baaaaa=b

Overlap of [2] aaba=b with [3] ab=baa:

a aba ab

Critical pair: abaaa=b.

Reduce LHS:

[3](ab)aaa
⇒ baaaaa

Defines rule #1.