Certificate for #10004 ⟨a, b | aa=1, ababba=bb⟩

Back:⟨a, b | aa=1, ababba=bb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

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

[2] ababba=bb

Axiom: ababba=bb.

Referenced by [3], [5].

[3] ababb=bba

Overlap of [2] ababba=bb with [1] aa=1:

ababb a aa

Critical pair: ababb=bba.

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

[4] babb=abba

Overlap of [1] aa=1 with [3] ababb=bba:

a a ababb

Critical pair: abba=babb.

Flip LHS and RHS.

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

[5] bbbb=abbb

Overlap of [2] ababba=bb with [4] babb=abba:

abab ba babb

Critical pair: abababba=bbbb.

Reduce LHS:

[3]ab(ababb)a
[1]⇒ abbb(aa)
⇒ abbb

Flip LHS and RHS.

Referenced by [6], [7].

[6] bbb=abb

Overlap of [3] ababb=bba with [5] bbbb=abbb:

aba bb bbbb

Critical pair: abaabbb=bbabb.

Reduce LHS:

[1]ab(aa)bbb
[5]⇒ a(bbbb)
[1]⇒ (aa)bbb
⇒ bbb

Reduce RHS:

[4]b(babb)
[4]⇒ (babb)a
[1]⇒ abb(aa)
⇒ abb

Defines rule #3.

Referenced by [7].

[7] bba=abb

Overlap of [5] bbbb=abbb with [4] babb=abba:

bbb b babb

Critical pair: bbbabba=abbbabb.

Reduce LHS:

[6](bbb)abba
[4]⇒ ab(babb)a
[3]⇒ (ababb)aa
[1]⇒ bb(aa)a
⇒ bba

Reduce RHS:

[6]a(bbb)abb
[1]⇒ (aa)bbabb
[4]⇒ b(babb)
[4]⇒ (babb)a
[1]⇒ abb(aa)
⇒ abb

Defines rule #2.

Referenced by [8].

[8] babb=bb

Simplify [4] babb=abba.

Reduce RHS:

[7]a(bba)
[1]⇒ (aa)bb
⇒ bb

Defines rule #4.