Certificate for #16471 ⟨a, b | aba=bb, bbbb=ab⟩

Back:⟨a, b | aba=bb, bbbb=ab⟩

Completion settings:

[1] aba=bb

Axiom: aba=bb.

Referenced by [3].

[2] ab=bbbb

Axiom: bbbb=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] bbbba=bb

Overlap of [1] aba=bb with [2] ab=bbbb:

aba ab

Critical pair: bbbba=bb.

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

[4] bbbbbbbb=bbb

Overlap of [3] bbbba=bb with [2] ab=bbbb:

bbbb a ab

Critical pair: bbbbbbbb=bbb.

Referenced by [5], [6].

[5] bbba=bbbbbb

Overlap of [4] bbbbbbbb=bbb with [3] bbbba=bb:

bbbb bbbb bbbba

Critical pair: bbbbbb=bbba.

Flip LHS and RHS.

Referenced by [6].

[6] bbbbbbb=bb

Overlap of [4] bbbbbbbb=bbb with [5] bbba=bbbbbb:

bbbbbb bb bbba

Critical pair: bbbbbbbbbbbb=bbbba.

Reduce LHS:

[4](bbbbbbbb)bbbb
⇒ bbbbbbb

Reduce RHS:

[3](bbbba)
⇒ bb

Defines rule #1.

Referenced by [7].

[7] bba=bbbbb

Overlap of [6] bbbbbbb=bb with [3] bbbba=bb:

bbb bbbb bbbba

Critical pair: bbbbb=bba.

Flip LHS and RHS.

Defines rule #3.