Certificate for #7816 ⟨a, b | aaa=1, babbb=ba⟩

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

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [4].

[2] babbb=ba

Axiom: babbb=ba.

Defines rule #3.

Referenced by [3], [4].

[3] baabbb=baa

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

babb b babbb

Critical pair: babbba=baabbb.

Reduce LHS:

[2](babbb)a
⇒ baa

Flip LHS and RHS.

Defines rule #4.

Referenced by [4].

[4] bbbb=b

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

babb b baabbb

Critical pair: babbbaa=baaabbb.

Reduce LHS:

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

Reduce RHS:

[1]b(aaa)bbb
⇒ bbbb

Flip LHS and RHS.

Defines rule #2.