Certificate for #7808 ⟨a, b | aaa=1, baabb=ab⟩

Back:⟨a, b | aaa=1, baabb=ab⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [4].

[2] baabb=ab

Axiom: baabb=ab.

Defines rule #2.

Referenced by [3], [4].

[3] baabab=aab

Overlap of [2] baabb=ab with [2] baabb=ab:

baab b baabb

Critical pair: baabab=abaabb.

Reduce RHS:

[2]a(baabb)
⇒ aab

Defines rule #3.

Referenced by [4].

[4] baabaab=b

Overlap of [2] baabb=ab with [3] baabab=aab:

baab b baabab

Critical pair: baabaab=abaabab.

Reduce RHS:

[3]a(baabab)
[1]⇒ (aaa)b
⇒ b

Defines rule #4.