Certificate for #15932 ⟨a, b | aba=bb, abbbb=b⟩

Back:⟨a, b | aba=bb, abbbb=b⟩

Completion settings:

[1] aba=bb

Axiom: aba=bb.

Referenced by [3], [4].

[2] abbbb=b

Axiom: abbbb=b.

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

[3] bbba=abbb

Overlap of [1] aba=bb with [1] aba=bb:

ab a aba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Referenced by [5].

[4] abb=bbbbbb

Overlap of [1] aba=bb with [2] abbbb=b:

ab a abbbb

Critical pair: abb=bbbbbb.

Referenced by [5], [6], [7], [8].

[5] bbba=bbbbbbb

Simplify [3] bbba=abbb.

Reduce RHS:

[4](abb)b
⇒ bbbbbbb

Referenced by [6], [8].

[6] ba=bbbbbbbbbbbb

Overlap of [2] abbbb=b with [5] bbba=bbbbbbb:

ab bbb bbba

Critical pair: abbbbbbbb=ba.

Reduce LHS:

[4](abb)bbbbbb
⇒ bbbbbbbbbbbb

Flip LHS and RHS.

Referenced by [8], [9].

[7] bbbbbbbb=b

Overlap of [2] abbbb=b with [4] abb=bbbbbb:

abbbb abb

Critical pair: bbbbbbbb=b.

Defines rule #1.

Referenced by [8], [9].

[8] ab=bbbbb

Overlap of [4] abb=bbbbbb with [5] bbba=bbbbbbb:

ab b bbba

Critical pair: abbbbbbbb=bbbbbbbba.

Reduce LHS:

[7]a(bbbbbbbb)
⇒ ab

Reduce RHS:

[7](bbbbbbbb)a
[6]⇒ (ba)
[7]⇒ (bbbbbbbb)bbbb
⇒ bbbbb

Defines rule #2.

[9] ba=bbbbb

Simplify [6] ba=bbbbbbbbbbbb.

Reduce RHS:

[7](bbbbbbbb)bbbb
⇒ bbbbb

Defines rule #3.