Certificate for #19598 ⟨a, b | aab=b, babbb=ba⟩

Back:⟨a, b | aab=b, babbb=ba⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #4.

Referenced by [3], [5].

[2] babbb=ba

Axiom: babbb=ba.

Defines rule #2.

Referenced by [3], [4].

[3] baa=bbbb

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

babb b babbb

Critical pair: babbba=baabbb.

Reduce LHS:

[2](babbb)a
⇒ baa

Reduce RHS:

[1]b(aab)bb
⇒ bbbb

Defines rule #5.

Referenced by [4], [5].

[4] bbbba=ba

Overlap of [2] babbb=ba with [3] baa=bbbb:

babb b baa

Critical pair: babbbbbb=baaa.

Reduce LHS:

[2](babbb)bbb
[2]⇒ (babbb)
⇒ ba

Reduce RHS:

[3](baa)a
⇒ bbbba

Flip LHS and RHS.

Defines rule #3.

[5] bbbbb=bb

Overlap of [3] baa=bbbb with [1] aab=b:

b aa aab

Critical pair: bb=bbbbb.

Flip LHS and RHS.

Defines rule #1.