Certificate for #23310 ⟨a, b | aaa=1, babb=abba⟩

Completion settings:

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

[1] aaa=1

Axiom: aaa=1.

Defines rule #8.

Referenced by [3], [4], [11], [14].

[2] abba=babb

Axiom: babb=abba.

Flip LHS and RHS.

Defines rule #4.

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

[3] aababb=bba

Overlap of [1] aaa=1 with [2] abba=babb:

aa a abba

Critical pair: aababb=bba.

Defines rule #9.

Referenced by [7], [12], [15], [18].

[4] bbbabb=abb

Overlap of [2] abba=babb with [1] aaa=1:

abb a aaa

Critical pair: abb=babbaa.

Reduce RHS:

[2]	b(abba)a
[2]	⇒ bb(abba)
	⇒ bbbabb

Flip LHS and RHS.

Referenced by [5], [6], [9], [13].

[5] babbbba=aabb

Overlap of [2] abba=babb with [2] abba=babb:

abb a abba

Critical pair: abbbabb=babbbba.

Reduce LHS:

[4]	a(bbbabb)
	⇒ aabb

Flip LHS and RHS.

Referenced by [8], [9], [14].

[6] bbbaabb=aabb

Overlap of [4] bbbabb=abb with [4] bbbabb=abb:

bbba bb bbbabb

Critical pair: bbbaabb=abbbabb.

Reduce RHS:

[4]	a(bbbabb)
	⇒ aabb

Referenced by [10].

[7] bbaa=ababbbb

Overlap of [3] aababb=bba with [2] abba=babb:

aab abb abba

Critical pair: aabbabb=bbaa.

Reduce LHS:

[2]	a(abba)bb
	⇒ ababbbb

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [14].

[8] abaabb=babbbbbba

Overlap of [2] abba=babb with [5] babbbba=aabb:

ab ba babbbba

Critical pair: abaabb=babbbbbba.

Referenced by [16].

[9] bababb=aabbbb

Overlap of [5] babbbba=aabb with [4] bbbabb=abb:

bab bbba bbbabb

Critical pair: bababb=aabbbb.

Defines rule #5.

Referenced by [10].

[10] aabbbbbbbb=aabb

Simplify [6] bbbaabb=aabb.

Reduce LHS:

[7]	b(bbaa)bb
[9]	⇒ (bababb)bbbb
	⇒ aabbbbbbbb

Referenced by [11].

[11] bbbbbbbb=bb

Overlap of [1] aaa=1 with [10] aabbbbbbbb=aabb:

a aa aabbbbbbbb

Critical pair: aaabb=bbbbbbbb.

Reduce LHS:

[1]	(aaa)bb
	⇒ bb

Flip LHS and RHS.

Referenced by [12], [14].

[12] bbabbbbbb=bba

Overlap of [3] aababb=bba with [11] bbbbbbbb=bb:

aaba bb bbbbbbbb

Critical pair: aababb=bbabbbbbb.

Reduce LHS:

[3]	(aababb)
	⇒ bba

Flip LHS and RHS.

Referenced by [13], [14].

[13] bbba=abbbbbb

Overlap of [4] bbbabb=abb with [12] bbabbbbbb=bba:

b bbabb bbabbbbbb

Critical pair: bbba=abbbbbb.

Referenced by [14], [16], [17].

[14] bbbbb=bb

Overlap of [12] bbabbbbbb=bba with [7] bbaa=ababbbb:

bbabbbb bb bbaa

Critical pair: bbabbbbababbbb=bbaaa.

Reduce LHS:

[5]	b(babbbba)babbbb
[13]	⇒ baa(bbba)bbbb
[1]	⇒ b(aaa)bbbbbbbbbb
[11]	⇒ (bbbbbbbb)bbb
	⇒ bbbbb

Reduce RHS:

[1]	bb(aaa)
	⇒ bb

Defines rule #1.

Referenced by [15], [16], [17], [18].

[15] bbabbb=bba

Overlap of [3] aababb=bba with [14] bbbbb=bb:

aaba bb bbbbb

Critical pair: aababb=bbabbb.

Reduce LHS:

[3]	(aababb)
	⇒ bba

Flip LHS and RHS.

Defines rule #2.

[16] abaabb=baabbb

Simplify [8] abaabb=babbbbbba.

Reduce RHS:

[14]	ba(bbbbb)ba
[13]	⇒ ba(bbba)
[14]	⇒ baa(bbbbb)b
	⇒ baabbb

Defines rule #10.

Referenced by [18].

[17] bbba=abbb

Simplify [13] bbba=abbbbbb.

Reduce RHS:

[14]	a(bbbbb)b
	⇒ abbb

Defines rule #3.

Referenced by [18].

[18] bbaba=baabb

Overlap of [3] aababb=bba with [17] bbba=abbb:

aaba bb bbba

Critical pair: aabaabbb=bbaba.

Reduce LHS:

[16]	a(abaabb)b
[16]	⇒ (abaabb)bb
[14]	⇒ baa(bbbbb)
	⇒ baabb

Flip LHS and RHS.

Defines rule #7.