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

Completion settings:

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

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [4], [5], [6], [8], [9], [10], [11], [12], [13], [14], [15].

[2] babb=abba

Axiom: babb=abba.

Defines rule #3.

Referenced by [3], [5], [7], [9], [10], [11], [14], [15], [18].

[3] abbaabb=baabbaa

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

bab b babb

Critical pair: bababba=abbaabb.

Reduce LHS:

[2]	ba(babb)a
	⇒ baabbaa

Flip LHS and RHS.

Referenced by [4], [5], [8], [15].

[4] bbaabb=aabaabbaa

Overlap of [1] aaa=1 with [3] abbaabb=baabbaa:

aa a abbaabb

Critical pair: aabaabbaa=bbaabb.

Flip LHS and RHS.

Referenced by [5], [8].

[5] abbbb=aabaabba

Overlap of [2] babb=abba with [3] abbaabb=baabbaa:

b abb abbaabb

Critical pair: bbaabbaa=abbaaabb.

Reduce LHS:

[4]	(bbaabb)aa
[1]	⇒ aabaabb(aaa)a
	⇒ aabaabba

Reduce RHS:

[1]	abb(aaa)bb
	⇒ abbbb

Flip LHS and RHS.

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

[6] bbbb=abaabba

Overlap of [1] aaa=1 with [5] abbbb=aabaabba:

aa a abbbb

Critical pair: aaaabaabba=bbbb.

Reduce LHS:

[1]	(aaa)abaabba
	⇒ abaabba

Flip LHS and RHS.

Referenced by [17].

[7] baabaabba=aabbaa

Overlap of [2] babb=abba with [5] abbbb=aabaabba:

b abb abbbb

Critical pair: baabaabba=abbabb.

Reduce RHS:

[2]	ab(babb)
[2]	⇒ a(babb)a
	⇒ aabbaa

Referenced by [8], [9].

[8] babaabbaa=bba

Overlap of [3] abbaabb=baabbaa with [5] abbbb=aabaabba:

abba abb abbbb

Critical pair: abbaaabaabba=baabbaabb.

Reduce LHS:

[1]	abb(aaa)baabba
[4]	⇒ ab(bbaabb)a
[7]	⇒ a(baabaabba)aa
[1]	⇒ (aaa)bbaaaa
[1]	⇒ bb(aaa)a
	⇒ bba

Reduce RHS:

[3]	ba(abbaabb)
	⇒ babaabbaa

Flip LHS and RHS.

Referenced by [9], [10], [11].

[9] abaabb=abbaba

Overlap of [2] babb=abba with [8] babaabbaa=bba:

bab b babaabbaa

Critical pair: babbba=abbaabaabbaa.

Reduce LHS:

[2]	(babb)ba
	⇒ abbaba

Reduce RHS:

[7]	ab(baabaabba)a
[1]	⇒ abaabb(aaa)
	⇒ abaabb

Flip LHS and RHS.

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

[10] abbaaba=bbaa

Overlap of [8] babaabbaa=bba with [1] aaa=1:

babaabb aa aaa

Critical pair: babaabb=bbaa.

Reduce LHS:

[9]	b(abaabb)
[2]	⇒ (babb)aba
	⇒ abbaaba

Referenced by [11], [12].

[11] baabb=bbaba

Overlap of [8] babaabbaa=bba with [10] abbaaba=bbaa:

baba abbaa abbaaba

Critical pair: bababbaa=bbaba.

Reduce LHS:

[2]	ba(babb)aa
[1]	⇒ baabb(aaa)
	⇒ baabb

Defines rule #4.

Referenced by [15], [18].

[12] abbaab=bba

Overlap of [10] abbaaba=bbaa with [1] aaa=1:

abbaab a aaa

Critical pair: abbaab=bbaaaa.

Reduce RHS:

[1]	bb(aaa)a
	⇒ bba

Referenced by [13], [14], [15].

[13] bbaab=aabba

Overlap of [1] aaa=1 with [12] abbaab=bba:

aa a abbaab

Critical pair: aabba=bbaab.

Flip LHS and RHS.

Defines rule #2.

[14] abbb=bbba

Overlap of [2] babb=abba with [12] abbaab=bba:

b abb abbaab

Critical pair: bbba=abbaaab.

Reduce RHS:

[1]	abb(aaa)b
	⇒ abbb

Flip LHS and RHS.

Defines rule #5.

Referenced by [16], [18].

[15] bbabaab=aabb

Overlap of [3] abbaabb=baabbaa with [12] abbaab=bba:

abba abb abbaab

Critical pair: abbabba=baabbaaaab.

Reduce LHS:

[2]	ab(babb)a
[2]	⇒ a(babb)aa
[1]	⇒ aabb(aaa)
	⇒ aabb

Reduce RHS:

[11]	(baabb)aaaab
[1]	⇒ bbab(aaa)aab
	⇒ bbabaab

Flip LHS and RHS.

Defines rule #9.

[16] bbbab=aabbabaa

Overlap of [5] abbbb=aabaabba with [14] abbb=bbba:

abbbb abbb

Critical pair: bbbab=aabaabba.

Reduce RHS:

[9]	a(abaabb)a
	⇒ aabbabaa

Defines rule #7.

[17] bbbb=abbabaa

Simplify [6] bbbb=abaabba.

Reduce RHS:

[9]	(abaabb)a
	⇒ abbabaa

Defines rule #6.

[18] bbabab=abbaba

Overlap of [11] baabb=bbaba with [14] abbb=bbba:

ba abb abbb

Critical pair: babbba=bbabab.

Reduce LHS:

[2]	(babb)ba
	⇒ abbaba

Flip LHS and RHS.

Defines rule #8.