Certificate for #11025 ⟨a, b | abba=aab, bbbb=1⟩

Completion settings:

Auxiliary generators:
1. c = bab
Reduction order:
- Left-to-right recursive path with deg(b) = deg(c) = 0, b < c; deg(a) = 1

[1] abba=aab

Axiom: abba=aab.

Referenced by [6].

[2] bbbb=1

Axiom: bbbb=1.

Defines rule #1.

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

[3] bab=c

Axiom: bab=c.

Referenced by [4], [6].

[4] ab=bbbc

Overlap of [2] bbbb=1 with [3] bab=c:

bbb b bab

Critical pair: bbbc=ab.

Flip LHS and RHS.

Referenced by [5].

[5] a=bbbcbbb

Overlap of [4] ab=bbbc with [2] bbbb=1:

a b bbbb

Critical pair: a=bbbcbbb.

Defines rule #5.

Referenced by [6].

[6] bbbccbbb=bbbcbbc

Simplify [1] abba=aab.

Reduce LHS:

[5]	(a)bba
[2]	⇒ bbbc(bbbb)ba
[5]	⇒ bbbcb(a)
[2]	⇒ bbbc(bbbb)cbbb
	⇒ bbbccbbb

Reduce RHS:

[5]	(a)ab
[3]	⇒ bbbcbb(bab)
	⇒ bbbcbbc

Referenced by [7].

[7] ccbbb=cbbc

Overlap of [2] bbbb=1 with [6] bbbccbbb=bbbcbbc:

b bbb bbbccbbb

Critical pair: bbbbcbbc=ccbbb.

Reduce LHS:

[2]	(bbbb)cbbc
	⇒ cbbc

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[8] cbbcb=cc

Overlap of [7] ccbbb=cbbc with [2] bbbb=1:

cc bbb bbbb

Critical pair: cc=cbbcb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[9] ccbcb=cbbcc

Overlap of [8] cbbcb=cc with [8] cbbcb=cc:

cbb cb cbbcb

Critical pair: cbbcc=ccbcb.

Flip LHS and RHS.

Defines rule #4.