Certificate for #27673 ⟨a, b | aa=1, abbabb=bbb⟩

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

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #4.

Referenced by [3], [5].

[2] abbabb=bbb

Axiom: abbabb=bbb.

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

[3] bbabb=abbb

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

a a abbabb

Critical pair: abbb=bbabb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] babbb=abbbbb

Overlap of [2] abbabb=bbb with [2] abbabb=bbb:

abb abb abbabb

Critical pair: abbbbb=bbbabb.

Reduce RHS:

[3]b(bbabb)
⇒ babbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] bbbbbbb=bbbb

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

bbab b bbabb

Critical pair: bbababbb=abbbbabb.

Reduce LHS:

[4]bba(babbb)
[1]⇒ bb(aa)bbbbb
⇒ bbbbbbb

Reduce RHS:

[3]abb(bbabb)
[2]⇒ (abbabb)b
⇒ bbbb

Defines rule #1.