Certificate for #16316 ⟨a, b | aab=bb, baba=bb⟩

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

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #1.

Referenced by [3], [8].

[2] baba=bb

Axiom: baba=bb.

Defines rule #5.

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

[3] babbb=bbab

Overlap of [2] baba=bb with [1] aab=bb:

bab a aab

Critical pair: babbb=bbab.

Referenced by [5].

[4] babb=bbba

Overlap of [2] baba=bb with [2] baba=bb:

ba ba baba

Critical pair: babb=bbba.

Defines rule #4.

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

[5] bbbab=bbab

Simplify [3] babbb=bbab.

Reduce LHS:

[4](babb)b
⇒ bbbab

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

[6] bbbb=bbb

Overlap of [5] bbbab=bbab with [2] baba=bb:

bb bab baba

Critical pair: bbbb=bbaba.

Reduce RHS:

[2]b(baba)
⇒ bbb

Defines rule #2.

Referenced by [7], [8].

[7] bbab=bbba

Overlap of [4] babb=bbba with [6] bbbb=bbb:

ba bb bbbb

Critical pair: babbb=bbbabb.

Reduce LHS:

[4](babb)b
[5]⇒ (bbbab)
⇒ bbab

Reduce RHS:

[5](bbbab)b
[4]⇒ b(babb)
[6]⇒ (bbbb)a
⇒ bbba

Defines rule #3.

Referenced by [8].

[8] bbbaa=bbb

Overlap of [4] babb=bbba with [7] bbab=bbba:

ba bb bbab

Critical pair: babbba=bbbaab.

Reduce LHS:

[4](babb)ba
[5]⇒ (bbbab)a
[7]⇒ (bbab)a
⇒ bbbaa

Reduce RHS:

[1]bbb(aab)
[6]⇒ (bbbb)b
[6]⇒ (bbbb)
⇒ bbb

Defines rule #6.