Certificate for #8061 ⟨a, b | aaa=1, abab=bbb⟩

Completion settings:

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

[1] aaa=1

Axiom: aaa=1.

Defines rule #9.

Referenced by [3].

[2] abab=bbb

Axiom: abab=bbb.

Defines rule #6.

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

[3] aabbb=bab

Overlap of [1] aaa=1 with [2] abab=bbb:

aa a abab

Critical pair: aabbb=bab.

Defines rule #5.

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

[4] bbbab=abbbb

Overlap of [2] abab=bbb with [2] abab=bbb:

ab ab abab

Critical pair: abbbb=bbbab.

Flip LHS and RHS.

Defines rule #4.

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

[5] abbabb=bbabbbb

Overlap of [2] abab=bbb with [4] bbbab=abbbb:

aba b bbbab

Critical pair: abaabbbb=bbbbbab.

Reduce LHS:

[3]	ab(aabbb)b
	⇒ abbabb

Reduce RHS:

[4]	bb(bbbab)
	⇒ bbabbbb

Defines rule #7.

Referenced by [7], [8].

[6] babbab=abbbbbb

Overlap of [3] aabbb=bab with [4] bbbab=abbbb:

aab bb bbbab

Critical pair: aababbbb=babbab.

Reduce LHS:

[2]	a(abab)bbb
	⇒ abbbbbb

Flip LHS and RHS.

Defines rule #8.

Referenced by [8].

[7] bbabbbbbbbb=bbabb

Overlap of [3] aabbb=bab with [4] bbbab=abbbb:

aabb b bbbab

Critical pair: aabbabbbb=babbbab.

Reduce LHS:

[5]	a(abbabb)bb
[5]	⇒ (abbabb)bbbb
	⇒ bbabbbbbbbb

Reduce RHS:

[4]	ba(bbbab)
[3]	⇒ b(aabbb)b
	⇒ bbabb

Defines rule #3.

[8] babbbbbbbbb=babbb

Overlap of [5] abbabb=bbabbbb with [4] bbbab=abbbb:

abba bb bbbab

Critical pair: abbaabbbb=bbabbbbbab.

Reduce LHS:

[3]	abb(aabbb)b
[4]	⇒ a(bbbab)b
[3]	⇒ (aabbb)bb
	⇒ babbb

Reduce RHS:

[4]	bbabb(bbbab)
[6]	⇒ b(babbab)bbb
	⇒ babbbbbbbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[9] bbbbbbbbbbb=bbbbb

Overlap of [2] abab=bbb with [8] babbbbbbbbb=babbb:

a bab babbbbbbbbb

Critical pair: ababbb=bbbbbbbbbbb.

Reduce LHS:

[2]	(abab)bb
	⇒ bbbbb

Flip LHS and RHS.

Defines rule #1.