Certificate for #20165 ⟨a, b | aab=b, bbba=bab⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #4.

Referenced by [3], [4].

[2] bab=bbba

Axiom: bbba=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbaa=bbbb

Overlap of [2] bab=bbba with [2] bab=bbba:

ba b bab

Critical pair: babbba=bbbaab.

Reduce LHS:

[2](bab)bba
[2]⇒ bb(bab)ba
[2]⇒ bbbb(bab)a
⇒ bbbbbbbaa

Reduce RHS:

[1]bbb(aab)
⇒ bbbb

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

[4] bbbbbbbb=bbbbb

Overlap of [3] bbbbbbbaa=bbbb with [1] aab=b:

bbbbbbb aa aab

Critical pair: bbbbbbbb=bbbbb.

Referenced by [5].

[5] bbbbbaa=bbbbb

Overlap of [4] bbbbbbbb=bbbbb with [3] bbbbbbbaa=bbbb:

b bbbbbbb bbbbbbbaa

Critical pair: bbbbb=bbbbbaa.

Flip LHS and RHS.

Referenced by [6], [7].

[6] bbbbbbb=bbbb

Overlap of [3] bbbbbbbaa=bbbb with [5] bbbbbaa=bbbbb:

bb bbbbbaa bbbbbaa

Critical pair: bbbbbbb=bbbb.

Defines rule #1.

Referenced by [7].

[7] bbbbaa=bbbb

Overlap of [6] bbbbbbb=bbbb with [5] bbbbbaa=bbbbb:

bb bbbbb bbbbbaa

Critical pair: bbbbbbb=bbbbaa.

Reduce LHS:

[6](bbbbbbb)
⇒ bbbb

Flip LHS and RHS.

Defines rule #3.