Certificate for #10301 ⟨a, b | aa=1, abbbb=bab⟩

Back:⟨a, b | aa=1, abbbb=bab⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #3.

Referenced by [3].

[2] bab=abbbb

Axiom: abbbb=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbbbbbbb=bbbbb

Overlap of [2] bab=abbbb with [2] bab=abbbb:

ba b bab

Critical pair: baabbbb=abbbbab.

Reduce LHS:

[1]b(aa)bbbb
⇒ bbbbb

Reduce RHS:

[2]abbb(bab)
[2]⇒ abb(bab)bbb
[2]⇒ ab(bab)bbbbbb
[2]⇒ a(bab)bbbbbbbbb
[1]⇒ (aa)bbbbbbbbbbbbb
⇒ bbbbbbbbbbbbb

Flip LHS and RHS.

Defines rule #1.