Certificate for #27657 ⟨a, b | aa=1, ababbb=bbb⟩

Back:⟨a, b | aa=1, ababbb=bbb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [3].

[2] ababbb=bbb

Axiom: ababbb=bbb.

Referenced by [3], [4].

[3] babbb=abbb

Overlap of [1] aa=1 with [2] ababbb=bbb:

a a ababbb

Critical pair: abbb=babbb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] bbbb=bbb

Overlap of [3] babbb=abbb with [3] babbb=abbb:

babb b babbb

Critical pair: babbabbb=abbbabbb.

Reduce LHS:

[3]bab(babbb)
[2]⇒ b(ababbb)
⇒ bbbb

Reduce RHS:

[3]abb(babbb)
[3]⇒ ab(babbb)
[2]⇒ (ababbb)
⇒ bbb

Defines rule #2.