Certificate for #15782 ⟨a, b | aab=bb, babba=b⟩

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

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

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

[2] babba=b

Axiom: babba=b.

Referenced by [3], [4].

[3] babb=bbba

Overlap of [2] babba=b with [2] babba=b:

bab ba babba

Critical pair: babb=bbba.

Referenced by [4], [6].

[4] bbbaa=b

Overlap of [2] babba=b with [3] babb=bbba:

babba babb

Critical pair: bbbaa=b.

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

[5] bbbbb=bb

Overlap of [4] bbbaa=b with [1] aab=bb:

bbb aa aab

Critical pair: bbbbb=bb.

Referenced by [6].

[6] bab=bba

Overlap of [4] bbbaa=b with [1] aab=bb:

bbba a aab

Critical pair: bbbabb=bab.

Reduce LHS:

[3]bb(babb)
[5]⇒ (bbbbb)a
⇒ bba

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] bbbb=b

Overlap of [6] bab=bba with [6] bab=bba:

ba b bab

Critical pair: babba=bbaab.

Reduce LHS:

[6](bab)ba
[6]⇒ b(bab)a
[4]⇒ (bbbaa)
⇒ b

Reduce RHS:

[1]bb(aab)
⇒ bbbb

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

[8] baa=bb

Overlap of [7] bbbb=b with [4] bbbaa=b:

b bbb bbbaa

Critical pair: bb=baa.

Flip LHS and RHS.

Defines rule #2.