Certificate for #15487 ⟨a, b | aaa=ab, babbb=a⟩

Back:⟨a, b | aaa=ab, babbb=a⟩

Completion settings:

[1] aaa=ab

Axiom: aaa=ab.

Defines rule #2.

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

[2] babbb=a

Axiom: babbb=a.

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

[3] aba=aab

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

a aa aaa

Critical pair: aab=aba.

Flip LHS and RHS.

Referenced by [4], [5].

[4] abba=aabb

Overlap of [1] aaa=ab with [3] aba=aab:

aa a aba

Critical pair: aaaab=abba.

Reduce LHS:

[1](aaa)ab
[3]⇒ (aba)b
⇒ aabb

Flip LHS and RHS.

Referenced by [6].

[5] aabbbb=aa

Overlap of [3] aba=aab with [2] babbb=a:

a ba babbb

Critical pair: aa=aabbbb.

Flip LHS and RHS.

Referenced by [6].

[6] abbbbb=ab

Overlap of [4] abba=aabb with [4] abba=aabb:

abb a abba

Critical pair: abbaabb=aabbbba.

Reduce LHS:

[4](abba)abb
[4]⇒ a(abba)bb
[1]⇒ (aaa)bbbb
⇒ abbbbb

Reduce RHS:

[5](aabbbb)a
[1]⇒ (aaa)
⇒ ab

Referenced by [7].

[7] bab=abb

Overlap of [2] babbb=a with [6] abbbbb=ab:

b abbb abbbbb

Critical pair: bab=abb.

Referenced by [8].

[8] abbbb=a

Overlap of [2] babbb=a with [7] bab=abb:

babbb bab

Critical pair: abbbb=a.

Defines rule #3.

Referenced by [9].

[9] ba=ab

Overlap of [2] babbb=a with [8] abbbb=a:

b abbb abbbb

Critical pair: ba=ab.

Defines rule #1.