Certificate for #425 ⟨a, b | aab=ba, bbb=1⟩

Back:⟨a, b | aab=ba, bbb=1⟩

Completion settings:

[1] aab=ba

Axiom: aab=ba.

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

[2] bbb=1

Axiom: bbb=1.

Defines rule #3.

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

[3] babb=aa

Overlap of [1] aab=ba with [2] bbb=1:

aa b bbb

Critical pair: aa=babb.

Flip LHS and RHS.

Referenced by [4].

[4] abb=bbaa

Overlap of [2] bbb=1 with [3] babb=aa:

bb b babb

Critical pair: bbaa=abb.

Flip LHS and RHS.

Referenced by [5].

[5] bab=bbaaaa

Overlap of [1] aab=ba with [4] abb=bbaa:

a ab abb

Critical pair: abbaa=bab.

Reduce LHS:

[4](abb)aa
⇒ bbaaaa

Flip LHS and RHS.

Referenced by [6], [7].

[6] bbaaaaaaaa=bba

Overlap of [1] aab=ba with [5] bab=bbaaaa:

aa b bab

Critical pair: aabbaaaa=baab.

Reduce LHS:

[1](aab)baaaa
[5]⇒ (bab)aaaa
⇒ bbaaaaaaaa

Reduce RHS:

[1]b(aab)
⇒ bba

Referenced by [8].

[7] ab=baaaa

Overlap of [2] bbb=1 with [5] bab=bbaaaa:

bb b bab

Critical pair: bbbbaaaa=ab.

Reduce LHS:

[2](bbb)baaaa
⇒ baaaa

Flip LHS and RHS.

Defines rule #2.

[8] aaaaaaaa=a

Overlap of [2] bbb=1 with [6] bbaaaaaaaa=bba:

b bb bbaaaaaaaa

Critical pair: bbba=aaaaaaaa.

Reduce LHS:

[2](bbb)a
⇒ a

Flip LHS and RHS.

Defines rule #1.