Certificate for #15435 ⟨a, b | aaa=aa, babbb=a⟩

Completion settings:

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

[1] aaa=aa

Axiom: aaa=aa.

Defines rule #1.

Referenced by [6], [9], [11], [16].

[2] babbb=a

Axiom: babbb=a.

Defines rule #10.

Referenced by [3], [4], [7], [8], [11], [15].

[3] babba=aabbb

Overlap of [2] babbb=a with [2] babbb=a:

babb b babbb

Critical pair: babba=aabbb.

Defines rule #6.

Referenced by [4], [5], [7], [9], [11], [13].

[4] aabbbbbb=baba

Overlap of [3] babba=aabbb with [2] babbb=a:

bab ba babbb

Critical pair: baba=aabbbbbb.

Flip LHS and RHS.

Defines rule #15.

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

[5] aabbbbba=babaabbb

Overlap of [3] babba=aabbb with [3] babba=aabbb:

bab ba babba

Critical pair: babaabbb=aabbbbba.

Flip LHS and RHS.

Referenced by [17].

[6] ababa=baba

Overlap of [1] aaa=aa with [4] aabbbbbb=baba:

a aa aabbbbbb

Critical pair: ababa=aabbbbbb.

Reduce RHS:

[4]	(aabbbbbb)
	⇒ baba

Defines rule #3.

Referenced by [7], [8], [9], [10], [12].

[7] aabbbbaba=aaba

Overlap of [3] babba=aabbb with [6] ababa=baba:

babb a ababa

Critical pair: babbbaba=aabbbbaba.

Reduce LHS:

[2]	(babbb)aba
	⇒ aaba

Flip LHS and RHS.

Referenced by [16], [18].

[8] abaa=baa

Overlap of [6] ababa=baba with [2] babbb=a:

aba ba babbb

Critical pair: abaa=bababbb.

Reduce RHS:

[2]	ba(babbb)
	⇒ baa

Defines rule #2.

Referenced by [9], [11], [12], [14], [17], [18].

[9] bbbaba=aabbbba

Overlap of [6] ababa=baba with [4] aabbbbbb=baba:

abab a aabbbbbb

Critical pair: ababbaba=babaabbbbbb.

Reduce LHS:

[3]	a(babba)ba
[1]	⇒ (aaa)bbbba
	⇒ aabbbba

Reduce RHS:

[8]	b(abaa)bbbbbb
[4]	⇒ bb(aabbbbbb)
	⇒ bbbaba

Flip LHS and RHS.

Defines rule #12.

Referenced by [18].

[10] abbaba=bbaba

Overlap of [6] ababa=baba with [6] ababa=baba:

ab aba ababa

Critical pair: abbaba=bababa.

Reduce RHS:

[6]	b(ababa)
	⇒ bbaba

Defines rule #8.

[11] aabbbbaa=aa

Overlap of [3] babba=aabbb with [8] abaa=baa:

babb a abaa

Critical pair: babbbaa=aabbbbaa.

Reduce LHS:

[2]	(babbb)aa
[1]	⇒ (aaa)
	⇒ aa

Flip LHS and RHS.

Referenced by [14].

[12] abbaa=bbaa

Overlap of [6] ababa=baba with [8] abaa=baa:

ab aba abaa

Critical pair: abbaa=babaa.

Reduce RHS:

[8]	b(abaa)
	⇒ bbaa

Defines rule #5.

Referenced by [13].

[13] bbbaa=aabbba

Overlap of [3] babba=aabbb with [12] abbaa=bbaa:

b abba abbaa

Critical pair: bbbaa=aabbba.

Defines rule #9.

Referenced by [14].

[14] baabbba=aa

Simplify [11] aabbbbaa=aa.

Reduce LHS:

[13]	aab(bbbaa)
[8]	⇒ a(abaa)bbba
[8]	⇒ (abaa)bbba
	⇒ baabbba

Defines rule #11.

Referenced by [15], [16].

[15] baabba=aabbb

Overlap of [14] baabbba=aa with [2] babbb=a:

baabb ba babbb

Critical pair: baabba=aabbb.

Defines rule #7.

[16] baaba=baba

Overlap of [14] baabbba=aa with [4] aabbbbbb=baba:

baabbb a aabbbbbb

Critical pair: baabbbbaba=aaabbbbbb.

Reduce LHS:

[7]	b(aabbbbaba)
	⇒ baaba

Reduce RHS:

[1]	(aaa)bbbbbb
[4]	⇒ (aabbbbbb)
	⇒ baba

Defines rule #4.

[17] aabbbbba=bbaabbb

Simplify [5] aabbbbba=babaabbb.

Reduce RHS:

[8]	b(abaa)bbb
	⇒ bbaabbb

Defines rule #13.

[18] baabbbba=aaba

Overlap of [7] aabbbbaba=aaba with [9] bbbaba=aabbbba:

aab bbbaba bbbaba

Critical pair: aabaabbbba=aaba.

Reduce LHS:

[8]	a(abaa)bbbba
[8]	⇒ (abaa)bbbba
	⇒ baabbbba

Defines rule #14.