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

Completion settings:

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

[1] aa=1

Axiom: aa=1.

Defines rule #4.

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

[2] abbbab=bb

Axiom: abbbab=bb.

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

[3] bbbab=abb

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

a a abbbab

Critical pair: abb=bbbab.

Flip LHS and RHS.

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

[4] babb=abbbbb

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

abbb ab abbbab

Critical pair: abbbbb=bbbbab.

Reduce RHS:

[3]	b(bbbab)
	⇒ babb

Flip LHS and RHS.

Defines rule #2.

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

[5] bbbbbbbbbbb=bbb

Overlap of [2] abbbab=bb with [4] babb=abbbbb:

abb bab babb

Critical pair: abbabbbbb=bbb.

Reduce LHS:

[4]	ab(babb)bbb
[4]	⇒ a(babb)bbbbbb
[1]	⇒ (aa)bbbbbbbbbbb
	⇒ bbbbbbbbbbb

Referenced by [6].

[6] abbbbbbbbbb=abb

Overlap of [5] bbbbbbbbbbb=bbb with [3] bbbab=abb:

bbbbbbbb bbb bbbab

Critical pair: bbbbbbbbabb=bbbab.

Reduce LHS:

[3]	bbbbb(bbbab)b
[3]	⇒ bb(bbbab)bb
[4]	⇒ b(babb)bb
[4]	⇒ (babb)bbbbb
	⇒ abbbbbbbbbb

Reduce RHS:

[3]	(bbbab)
	⇒ abb

Referenced by [7].

[7] bbbbbbbbbb=bb

Overlap of [1] aa=1 with [6] abbbbbbbbbb=abb:

a a abbbbbbbbbb

Critical pair: aabb=bbbbbbbbbb.

Reduce LHS:

[1]	(aa)bb
	⇒ bb

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] bbab=abbbbbbb

Overlap of [7] bbbbbbbbbb=bb with [3] bbbab=abb:

bbbbbbb bbb bbbab

Critical pair: bbbbbbbabb=bbab.

Reduce LHS:

[3]	bbbb(bbbab)b
[3]	⇒ b(bbbab)bb
[4]	⇒ (babb)bb
	⇒ abbbbbbb

Flip LHS and RHS.

Defines rule #3.