Certificate for #19559 ⟨a, b | aab=b, abbab=bb⟩

Back:⟨a, b | aab=b, abbab=bb⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

Referenced by [3], [5].

[2] abbab=bb

Axiom: abbab=bb.

Referenced by [3], [4].

[3] abb=bbab

Overlap of [1] aab=b with [2] abbab=bb:

a ab 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] aab=b with [3] abb=bbab:

a ab 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.