Certificate for #14872 ⟨a, b | abba=b, bbbbb=b⟩

Back:⟨a, b | abba=b, bbbbb=b⟩

Completion settings:

[1] abba=b

Axiom: abba=b.

Referenced by [3], [6].

[2] bbbbb=b

Axiom: bbbbb=b.

Defines rule #1.

Referenced by [4], [5], [7].

[3] bbba=abbb

Overlap of [1] abba=b with [1] abba=b:

abb a abba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Referenced by [4], [5], [6].

[4] bba=abb

Overlap of [2] bbbbb=b with [3] bbba=abbb:

bbb bb bbba

Critical pair: bbbabbb=bba.

Reduce LHS:

[3](bbba)bbb
[2]⇒ a(bbbbb)b
⇒ abb

Flip LHS and RHS.

Referenced by [5].

[5] ba=ab

Overlap of [2] bbbbb=b with [4] bba=abb:

bbb bb bba

Critical pair: bbbabb=ba.

Reduce LHS:

[3](bbba)bb
[2]⇒ a(bbbbb)
⇒ ab

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] aabbb=bb

Overlap of [5] ba=ab with [1] abba=b:

b a abba

Critical pair: bb=abbba.

Reduce RHS:

[3]a(bbba)
⇒ aabbb

Flip LHS and RHS.

Referenced by [7].

[7] aab=bbbb

Overlap of [6] aabbb=bb with [2] bbbbb=b:

aa bbb bbbbb

Critical pair: aab=bbbb.

Defines rule #3.