Certificate for #14484 ⟨a, b | aaab=b, aabab=b⟩

Back:⟨a, b | aaab=b, aabab=b⟩

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Defines rule #3.

Referenced by [3], [5].

[2] aabab=b

Axiom: aabab=b.

Referenced by [3].

[3] bab=ab

Overlap of [1] aaab=b with [2] aabab=b:

a aab aabab

Critical pair: ab=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] baab=aab

Overlap of [3] bab=ab with [3] bab=ab:

ba b bab

Critical pair: baab=abab.

Reduce RHS:

[3]a(bab)
⇒ aab

Defines rule #4.

Referenced by [5].

[5] bb=b

Overlap of [3] bab=ab with [4] baab=aab:

ba b baab

Critical pair: baaab=abaab.

Reduce LHS:

[1]b(aaab)
⇒ bb

Reduce RHS:

[4]a(baab)
[1]⇒ (aaab)
⇒ b

Defines rule #1.