Certificate for #2591 ⟨a, b | aaa=1, babb=ba⟩

Back:⟨a, b | aaa=1, babb=ba⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [4].

[2] babb=ba

Axiom: babb=ba.

Defines rule #3.

Referenced by [3], [4].

[3] baabb=baa

Overlap of [2] babb=ba with [2] babb=ba:

bab b babb

Critical pair: babba=baabb.

Reduce LHS:

[2](babb)a
⇒ baa

Flip LHS and RHS.

Defines rule #4.

Referenced by [4].

[4] bbb=b

Overlap of [2] babb=ba with [3] baabb=baa:

bab b baabb

Critical pair: babbaa=baaabb.

Reduce LHS:

[2](babb)aa
[1]⇒ b(aaa)
⇒ b

Reduce RHS:

[1]b(aaa)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #2.