Certificate for #24183 ⟨a, b | aa=a, bbabbbb=b⟩

Back:⟨a, b | aa=a, bbabbbb=b⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

[2] bbabbbb=b

Axiom: bbabbbb=b.

Referenced by [3], [4].

[3] bbabbb=babbbb

Overlap of [2] bbabbbb=b with [2] bbabbbb=b:

bbabb bb bbabbbb

Critical pair: bbabbb=babbbb.

Referenced by [4], [5].

[4] babbbbb=b

Overlap of [2] bbabbbb=b with [3] bbabbb=babbbb:

bbabbbb bbabbb

Critical pair: babbbbb=b.

Defines rule #3.

Referenced by [5].

[5] bbab=babb

Overlap of [3] bbabbb=babbbb with [3] bbabbb=babbbb:

bbab bb bbabbb

Critical pair: bbabbabbbb=babbbbabbb.

Reduce LHS:

[3]bba(bbabbb)b
[4]⇒ bba(babbbbb)
⇒ bbab

Reduce RHS:

[3]babb(bbabbb)
[3]⇒ bab(bbabbb)b
[3]⇒ ba(bbabbb)bb
[4]⇒ ba(babbbbb)b
⇒ babb

Defines rule #2.