Certificate for #12415 ⟨a, b | aaba=bb, baaa=b⟩

Back:⟨a, b | aaba=bb, baaa=b⟩

Completion settings:

[1] aaba=bb

Axiom: aaba=bb.

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

[2] baaa=b

Axiom: baaa=b.

Defines rule #4.

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

[3] aab=bbaa

Overlap of [1] aaba=bb with [2] baaa=b:

aa ba baaa

Critical pair: aab=bbaa.

Defines rule #3.

Referenced by [5], [6].

[4] babb=bba

Overlap of [2] baaa=b with [1] aaba=bb:

ba aa aaba

Critical pair: babb=bba.

Referenced by [7].

[5] bbab=bbbbbba

Overlap of [1] aaba=bb with [3] aab=bbaa:

aab a aab

Critical pair: aabbbaa=bbab.

Reduce LHS:

[3](aab)bbaa
[3]⇒ bb(aab)baa
[3]⇒ bbbb(aab)aa
[2]⇒ bbbbb(baaa)a
⇒ bbbbbba

Flip LHS and RHS.

Referenced by [7].

[6] bab=bbbbba

Overlap of [2] baaa=b with [3] aab=bbaa:

baa a aab

Critical pair: baabbaa=bab.

Reduce LHS:

[3]b(aab)baa
[3]⇒ bbb(aab)aa
[2]⇒ bbbb(baaa)a
⇒ bbbbba

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[7] bbbbbbbbba=bba

Overlap of [4] babb=bba with [6] bab=bbbbba:

babb bab

Critical pair: bbbbbab=bba.

Reduce LHS:

[5]bbb(bbab)
⇒ bbbbbbbbba

Referenced by [8].

[8] bbbbbbbbb=bb

Overlap of [7] bbbbbbbbba=bba with [2] baaa=b:

bbbbbbbb ba baaa

Critical pair: bbbbbbbbb=bbaaa.

Reduce RHS:

[2]b(baaa)
⇒ bb

Defines rule #1.