Certificate for #2437 ⟨a, b | aaa=1, ababb=b⟩

Back:⟨a, b | aaa=1, ababb=b⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [3], [6].

[2] ababb=b

Axiom: ababb=b.

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

[3] babb=aab

Overlap of [1] aaa=1 with [2] ababb=b:

aa a ababb

Critical pair: aab=babb.

Flip LHS and RHS.

Defines rule #2.

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

[4] ababaab=aab

Overlap of [2] ababb=b with [3] babb=aab:

abab b babb

Critical pair: ababaab=babb.

Reduce RHS:

[3](babb)
⇒ aab

Referenced by [6].

[5] babaab=ab

Overlap of [3] babb=aab with [3] babb=aab:

bab b babb

Critical pair: babaab=aababb.

Reduce RHS:

[2]a(ababb)
⇒ ab

Defines rule #4.

Referenced by [6].

[6] babab=b

Overlap of [3] babb=aab with [5] babaab=ab:

bab b babaab

Critical pair: babab=aababaab.

Reduce RHS:

[4]a(ababaab)
[1]⇒ (aaa)b
⇒ b

Defines rule #3.