Certificate for #28197 ⟨a, b | aa=1, abbab=bbbb⟩

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

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #4.

Referenced by [3], [7].

[2] abbab=bbbb

Axiom: abbab=bbbb.

Referenced by [3], [4].

[3] bbab=abbbb

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

a a abbab

Critical pair: abbbb=bbab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] babbbbbbb=abbbbbb

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

abb ab abbab

Critical pair: abbbbbb=bbbbbab.

Reduce RHS:

[3]bbb(bbab)
[3]⇒ b(bbab)bbb
⇒ babbbbbbb

Flip LHS and RHS.

Referenced by [5], [6].

[5] babbbbbb=abbbbbbbbbb

Overlap of [3] bbab=abbbb with [4] babbbbbbb=abbbbbb:

b bab babbbbbbb

Critical pair: babbbbbb=abbbbbbbbbb.

Defines rule #2.

Referenced by [6].

[6] abbbbbbbbbbb=abbbbbb

Overlap of [4] babbbbbbb=abbbbbb with [5] babbbbbb=abbbbbbbbbb:

babbbbbbb babbbbbb

Critical pair: abbbbbbbbbbb=abbbbbb.

Referenced by [7].

[7] bbbbbbbbbbb=bbbbbb

Overlap of [1] aa=1 with [6] abbbbbbbbbbb=abbbbbb:

a a abbbbbbbbbbb

Critical pair: aabbbbbb=bbbbbbbbbbb.

Reduce LHS:

[1](aa)bbbbbb
⇒ bbbbbb

Flip LHS and RHS.

Defines rule #1.