Certificate for #5065 ⟨a, b | aaa=ab, babb=b⟩

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

Completion settings:

[1] aaa=ab

Axiom: aaa=ab.

Defines rule #4.

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

[2] babb=b

Axiom: babb=b.

Referenced by [5], [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 [7].

[5] aabbb=ab

Overlap of [3] aba=aab with [2] babb=b:

a ba babb

Critical pair: ab=aabbb.

Flip LHS and RHS.

Referenced by [6].

[6] aab=abbbb

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

a aa aabbb

Critical pair: aab=abbbb.

Defines rule #3.

Referenced by [7].

[7] abba=abbbbb

Simplify [4] abba=aabb.

Reduce RHS:

[6](aab)b
⇒ abbbbb

Referenced by [8].

[8] ba=bbbb

Overlap of [2] babb=b with [7] abba=abbbbb:

b abb abba

Critical pair: babbbbb=ba.

Reduce LHS:

[2](babb)bbb
⇒ bbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[9] bbbbbb=b

Overlap of [2] babb=b with [8] ba=bbbb:

babb ba

Critical pair: bbbbbb=b.

Defines rule #1.