Certificate for #13247 ⟨a, b | bab=aaa, bba=bb⟩

Back:⟨a, b | bab=aaa, bba=bb⟩

Completion settings:

[1] aaa=bab

Axiom: bab=aaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[2] bba=bb

Axiom: bba=bb.

Defines rule #1.

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

[3] abab=baba

Overlap of [1] aaa=bab with [1] aaa=bab:

a aa aaa

Critical pair: abab=baba.

Defines rule #5.

Referenced by [5], [6].

[4] bbbb=bb

Overlap of [2] bba=bb with [1] aaa=bab:

bb a aaa

Critical pair: bbbab=bbaa.

Reduce LHS:

[2]b(bba)b
⇒ bbbb

Reduce RHS:

[2](bba)a
[2]⇒ (bba)
⇒ bb

Defines rule #4.

Referenced by [6].

[5] babaab=abbb

Overlap of [3] abab=baba with [3] abab=baba:

ab ab abab

Critical pair: abbaba=babaab.

Reduce LHS:

[2]a(bba)ba
[2]⇒ ab(bba)
⇒ abbb

Flip LHS and RHS.

Referenced by [6], [7].

[6] abb=bb

Overlap of [5] babaab=abbb with [3] abab=baba:

baba ab abab

Critical pair: babababa=abbbab.

Reduce LHS:

[3]b(abab)aba
[2]⇒ (bba)baaba
[2]⇒ b(bba)aba
[2]⇒ b(bba)ba
[4]⇒ (bbbb)a
[2]⇒ (bba)
⇒ bb

Reduce RHS:

[2]ab(bba)b
[4]⇒ a(bbbb)
⇒ abb

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[7] babaab=bbb

Simplify [5] babaab=abbb.

Reduce RHS:

[6](abb)b
⇒ bbb

Defines rule #6.