Certificate for #15372 ⟨a, b | aba=bb, aaabbb=1⟩

Completion settings:

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

[1] aba=bb

Axiom: aba=bb.

Defines rule #4.

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

[2] aaabbb=1

Axiom: aaabbb=1.

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

[3] bbba=abbb

Overlap of [1] aba=bb with [1] aba=bb:

ab a aba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #2.

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

[4] bbaabbb=ab

Overlap of [1] aba=bb with [2] aaabbb=1:

ab a aaabbb

Critical pair: ab=bbaabbb.

Flip LHS and RHS.

Referenced by [8].

[5] aabbbbb=ba

Overlap of [2] aaabbb=1 with [3] bbba=abbb:

aaab bb bbba

Critical pair: aaababbb=ba.

Reduce LHS:

[1]	aa(aba)bbb
	⇒ aabbbbb

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

[6] abba=bbabbbbb

Overlap of [1] aba=bb with [5] aabbbbb=ba:

ab a aabbbbb

Critical pair: abba=bbabbbbb.

Defines rule #5.

Referenced by [7].

[7] baa=bbabbbbbbbbbbbbb

Overlap of [5] aabbbbb=ba with [3] bbba=abbb:

aabb bbb bbba

Critical pair: aabbabbb=baa.

Reduce LHS:

[6]	a(abba)bbb
[6]	⇒ (abba)bbbbbbbb
	⇒ bbabbbbbbbbbbbbb

Flip LHS and RHS.

Referenced by [8].

[8] abbbbbbbbbbbbbbbbbbb=ab

Simplify [4] bbaabbb=ab.

Reduce LHS:

[7]	b(baa)bbb
[3]	⇒ (bbba)bbbbbbbbbbbbbbbb
	⇒ abbbbbbbbbbbbbbbbbbb

Referenced by [9].

[9] aab=babbbbbbbbbbbbbb

Overlap of [5] aabbbbb=ba with [8] abbbbbbbbbbbbbbbbbbb=ab:

a abbbbb abbbbbbbbbbbbbbbbbbb

Critical pair: aab=babbbbbbbbbbbbbb.

Referenced by [10], [11].

[10] bbbbbbbbbbbbbbbbbb=1

Overlap of [2] aaabbb=1 with [9] aab=babbbbbbbbbbbbbb:

a aabbb aab

Critical pair: ababbbbbbbbbbbbbbbb=1.

Reduce LHS:

[1]	(aba)bbbbbbbbbbbbbbbb
	⇒ bbbbbbbbbbbbbbbbbb

Defines rule #1.

Referenced by [11].

[11] aa=babbbbbbbbbbbbb

Overlap of [9] aab=babbbbbbbbbbbbbb with [10] bbbbbbbbbbbbbbbbbb=1:

aa b bbbbbbbbbbbbbbbbbb

Critical pair: aa=babbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

[10]	ba(bbbbbbbbbbbbbbbbbb)bbbbbbbbbbbbb
	⇒ babbbbbbbbbbbbb

Defines rule #3.