Certificate for #5219 ⟨a, b | aab=bb, bbba=b⟩

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

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

Referenced by [3], [6].

[2] bbba=b

Axiom: bbba=b.

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

[3] bab=bbbbb

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

bbb a aab

Critical pair: bbbbb=bab.

Flip LHS and RHS.

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

[4] bbbbbbb=bb

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

bb ba bab

Critical pair: bbbbbbb=bb.

Referenced by [5].

[5] bba=bbbbb

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

ba b bbba

Critical pair: bab=bbbbbbba.

Reduce LHS:

[3](bab)
⇒ bbbbb

Reduce RHS:

[4](bbbbbbb)a
⇒ bba

Flip LHS and RHS.

Referenced by [6], [7].

[6] bbbbbb=b

Overlap of [1] aab=bb with [5] bba=bbbbb:

aa b bba

Critical pair: aabbbbb=bbba.

Reduce LHS:

[1](aab)bbbb
⇒ bbbbbb

Reduce RHS:

[2](bbba)
⇒ b

Defines rule #1.

Referenced by [7].

[7] ba=bbbb

Overlap of [3] bab=bbbbb with [5] bba=bbbbb:

ba b bba

Critical pair: babbbbb=bbbbbba.

Reduce LHS:

[3](bab)bbbb
[6]⇒ (bbbbbb)bbb
⇒ bbbb

Reduce RHS:

[6](bbbbbb)a
⇒ ba

Flip LHS and RHS.

Defines rule #2.