Certificate for #19288 ⟨a, b | aaa=a, baabb=ab⟩

Completion settings:

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

[1] aaa=a

Axiom: aaa=a.

Defines rule #4.

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

[2] baabb=ab

Axiom: baabb=ab.

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

[3] baabab=aab

Overlap of [2] baabb=ab with [2] baabb=ab:

baab b baabb

Critical pair: baabab=abaabb.

Reduce RHS:

[2]	a(baabb)
	⇒ aab

Referenced by [4], [6].

[4] baabaab=ab

Overlap of [2] baabb=ab with [3] baabab=aab:

baab b baabab

Critical pair: baabaab=abaabab.

Reduce RHS:

[3]	a(baabab)
[1]	⇒ (aaa)b
	⇒ ab

Referenced by [5], [6].

[5] bab=abb

Overlap of [4] baabaab=ab with [2] baabb=ab:

baa baab baabb

Critical pair: baaab=abb.

Reduce LHS:

[1]	b(aaa)b
	⇒ bab

Defines rule #2.

Referenced by [6], [7], [10].

[6] baab=aabb

Overlap of [4] baabaab=ab with [3] baabab=aab:

baa baab baabab

Critical pair: baaaab=abab.

Reduce LHS:

[1]	b(aaa)ab
	⇒ baab

Reduce RHS:

[5]	a(bab)
	⇒ aabb

Referenced by [7], [8].

[7] aabb=abbbb

Overlap of [2] baabb=ab with [5] bab=abb:

baab b bab

Critical pair: baababb=abab.

Reduce LHS:

[6]	(baab)abb
[5]	⇒ aab(bab)b
[5]	⇒ aa(bab)bb
[1]	⇒ (aaa)bbbb
	⇒ abbbb

Reduce RHS:

[5]	a(bab)
	⇒ aabb

Flip LHS and RHS.

Referenced by [8].

[8] baab=abbbb

Simplify [6] baab=aabb.

Reduce RHS:

[7]	(aabb)
	⇒ abbbb

Referenced by [9], [10].

[9] abbbbb=ab

Overlap of [2] baabb=ab with [8] baab=abbbb:

baabb baab

Critical pair: abbbbb=ab.

Defines rule #1.

Referenced by [10].

[10] aab=abbb

Overlap of [5] bab=abb with [8] baab=abbbb:

ba b baab

Critical pair: baabbbb=abbaab.

Reduce LHS:

[8]	(baab)bbb
[9]	⇒ (abbbbb)bb
	⇒ abbb

Reduce RHS:

[8]	ab(baab)
[5]	⇒ a(bab)bbb
[9]	⇒ a(abbbbb)
	⇒ aab

Flip LHS and RHS.

Defines rule #3.