Certificate for #12315 ⟨a, b | aaab=bb, baba=b⟩

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

Completion settings:

[1] aaab=bb

Axiom: aaab=bb.

Defines rule #3.

Referenced by [4].

[2] baba=b

Axiom: baba=b.

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

[3] bba=bab

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

ba ba baba

Critical pair: bab=bba.

Flip LHS and RHS.

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

[4] bab=bbbb

Overlap of [3] bba=bab with [1] aaab=bb:

bb a aaab

Critical pair: bbbb=babaab.

Reduce RHS:

[2](baba)ab
⇒ bab

Flip LHS and RHS.

Referenced by [5], [6].

[5] bbbbbb=b

Overlap of [2] baba=b with [4] bab=bbbb:

baba bab

Critical pair: bbbba=b.

Reduce LHS:

[3]bb(bba)
[3]⇒ b(bba)b
[3]⇒ (bba)bb
[4]⇒ (bab)bb
⇒ bbbbbb

Defines rule #1.

Referenced by [6].

[6] ba=bbb

Overlap of [5] bbbbbb=b with [3] bba=bab:

bbbb bb bba

Critical pair: bbbbbab=ba.

Reduce LHS:

[3]bbb(bba)b
[3]⇒ bb(bba)bb
[3]⇒ b(bba)bbb
[3]⇒ (bba)bbbb
[4]⇒ (bab)bbbb
[5]⇒ (bbbbbb)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #2.