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

Completion settings:

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

[1] aaa=a

Axiom: aaa=a.

Defines rule #6.

Referenced by [3].

[2] abab=bbb

Axiom: abab=bbb.

Defines rule #5.

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

[3] aabbb=bbb

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

aa a abab

Critical pair: aabbb=abab.

Reduce RHS:

[2]	(abab)
	⇒ bbb

Defines rule #4.

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

Referenced by [5], [6].

[5] bbabbbb=abbbbb

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

aba b bbbab

Critical pair: abaabbbb=bbbbbab.

Reduce LHS:

[3]	ab(aabbb)b
	⇒ abbbbb

Reduce RHS:

[4]	bb(bbbab)
	⇒ bbabbbb

Flip LHS and RHS.

Referenced by [7].

[6] babbbb=abbbbbb

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

aab bb bbbab

Critical pair: aababbbb=bbbbab.

Reduce LHS:

[2]	a(abab)bbb
	⇒ abbbbbb

Reduce RHS:

[4]	b(bbbab)
	⇒ babbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[7] abbbbbbbb=abbbbb

Simplify [5] bbabbbb=abbbbb.

Reduce LHS:

[6]	b(babbbb)
[6]	⇒ (babbbb)bb
	⇒ abbbbbbbb

Referenced by [8].

[8] bbbbbbbb=bbbbb

Overlap of [3] aabbb=bbb with [7] abbbbbbbb=abbbbb:

a abbb abbbbbbbb

Critical pair: aabbbbb=bbbbbbbb.

Reduce LHS:

[3]	(aabbb)bb
	⇒ bbbbb

Flip LHS and RHS.

Defines rule #1.