Certificate for #20156 ⟨a, b | aab=b, bbab=baa⟩

Back:⟨a, b | aab=b, bbab=baa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3].

[2] bbab=baa

Axiom: bbab=baa.

Defines rule #2.

Referenced by [3].

[3] baaaa=baa

Overlap of [2] bbab=baa with [2] bbab=baa:

bba b bbab

Critical pair: bbabaa=baabab.

Reduce LHS:

[2](bbab)aa
⇒ baaaa

Reduce RHS:

[1]b(aab)ab
[2]⇒ (bbab)
⇒ baa

Defines rule #3.