Certificate for #16319 ⟨a, b | aab=bb, babb=ba⟩

Back:⟨a, b | aab=bb, babb=ba⟩

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #5.

Referenced by [3], [5].

[2] babb=ba

Axiom: babb=ba.

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

[3] baa=bbbb

Overlap of [2] babb=ba with [2] babb=ba:

bab b babb

Critical pair: babba=baabb.

Reduce LHS:

[2](babb)a
⇒ baa

Reduce RHS:

[1]b(aab)b
⇒ bbbb

Defines rule #4.

Referenced by [4], [5].

[4] bab=bbbba

Overlap of [2] babb=ba with [3] baa=bbbb:

bab b baa

Critical pair: babbbbb=baaa.

Reduce LHS:

[2](babb)bbb
[2]⇒ (babb)b
⇒ bab

Reduce RHS:

[3](baa)a
⇒ bbbba

Referenced by [6], [7].

[5] bbbbb=bbb

Overlap of [3] baa=bbbb with [1] aab=bb:

b aa aab

Critical pair: bbb=bbbbb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [6].

[6] bbba=ba

Overlap of [2] babb=ba with [4] bab=bbbba:

babb bab

Critical pair: bbbbab=ba.

Reduce LHS:

[4]bbb(bab)
[5]⇒ (bbbbb)bba
[5]⇒ (bbbbb)a
⇒ bbba

Defines rule #2.

Referenced by [7].

[7] bab=bba

Simplify [4] bab=bbbba.

Reduce RHS:

[6]b(bbba)
⇒ bba

Defines rule #3.