Certificate for #10020 ⟨a, b | aa=1, abbbab=bb⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(b) = 0; deg(a) = 1

[1] aa=1

Axiom: aa=1.

Defines rule #3.

Referenced by [3], [5].

[2] abbbab=bb

Axiom: abbbab=bb.

Referenced by [3], [4].

[3] abb=bbbab

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

a a abbbab

Critical pair: abb=bbbab.

Defines rule #2.

Referenced by [4], [5].

[4] bbbbbbbbbbbbab=bbbbab

Overlap of [2] abbbab=bb with [2] abbbab=bb:

abbb ab abbbab

Critical pair: abbbbb=bbbbab.

Reduce LHS:

[3]	(abb)bbb
[3]	⇒ bbb(abb)bb
[3]	⇒ bbbbbb(abb)b
[3]	⇒ bbbbbbbbb(abb)
	⇒ bbbbbbbbbbbbab

Referenced by [6].

[5] bbbbbbabab=bb

Overlap of [1] aa=1 with [3] abb=bbbab:

a a abb

Critical pair: abbbab=bb.

Reduce LHS:

[3]	(abb)bab
[3]	⇒ bbb(abb)ab
	⇒ bbbbbbabab

Referenced by [6], [7].

[6] bbbbabab=bbbbbbbb

Overlap of [4] bbbbbbbbbbbbab=bbbbab with [5] bbbbbbabab=bb:

bbbbbb bbbbbbab bbbbbbabab

Critical pair: bbbbbbbb=bbbbabab.

Flip LHS and RHS.

Referenced by [7], [8].

[7] bbbbbbbbbb=bb

Overlap of [5] bbbbbbabab=bb with [6] bbbbabab=bbbbbbbb:

bb bbbbabab bbbbabab

Critical pair: bbbbbbbbbb=bb.

Defines rule #1.

Referenced by [8].

[8] bbabab=bbbbbb

Overlap of [7] bbbbbbbbbb=bb with [6] bbbbabab=bbbbbbbb:

bbbbbb bbbb bbbbabab

Critical pair: bbbbbbbbbbbbbb=bbabab.

Reduce LHS:

[7]	(bbbbbbbbbb)bbbb
	⇒ bbbbbb

Flip LHS and RHS.

Defines rule #4.