Certificate for #3516 ⟨a, b | aa=1, abbab=bb⟩

Back:⟨a, b | aa=1, abbab=bb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #3.

Referenced by [3], [5].

[2] abbab=bb

Axiom: abbab=bb.

Referenced by [3], [4].

[3] abb=bbab

Overlap of [1] aa=1 with [2] abbab=bb:

a a abbab

Critical pair: abb=bbab.

Defines rule #2.

Referenced by [4], [5].

[4] bbbbbbab=bbbab

Overlap of [2] abbab=bb with [2] abbab=bb:

abb ab abbab

Critical pair: abbbb=bbbab.

Reduce LHS:

[3](abb)bb
[3]⇒ bb(abb)b
[3]⇒ bbbb(abb)
⇒ bbbbbbab

Referenced by [6].

[5] bbabab=bb

Overlap of [1] aa=1 with [3] abb=bbab:

a a abb

Critical pair: abbab=bb.

Reduce LHS:

[3](abb)ab
⇒ bbabab

Defines rule #4.

Referenced by [6].

[6] bbbbbb=bbb

Overlap of [4] bbbbbbab=bbbab with [5] bbabab=bb:

bbbb bbab bbabab

Critical pair: bbbbbb=bbbabab.

Reduce RHS:

[5]b(bbabab)
⇒ bbb

Defines rule #1.