Certificate for #26619 ⟨a, b | aa=1, abbabbba=b⟩

Completion settings:

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

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [3], [4], [5], [8], [9], [10], [12], [15], [17], [18], [20], [21].

[2] abbabbba=b

Axiom: abbabbba=b.

Referenced by [3].

[3] abbabbb=ba

Overlap of [2] abbabbba=b with [1] aa=1:

abbabbb a aa

Critical pair: abbabbb=ba.

Referenced by [4], [7], [11], [12], [14], [18].

[4] bbabbb=aba

Overlap of [1] aa=1 with [3] abbabbb=ba:

a a abbabbb

Critical pair: aba=bbabbb.

Flip LHS and RHS.

Defines rule #7.

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

[5] bbababa=abbbb

Overlap of [4] bbabbb=aba with [4] bbabbb=aba:

bbab bb bbabbb

Critical pair: bbababa=abaabbb.

Reduce RHS:

[1]	ab(aa)bbb
	⇒ abbbb

Defines rule #5.

Referenced by [7], [8], [9], [15], [18].

[6] bbabbaba=abababbb

Overlap of [4] bbabbb=aba with [4] bbabbb=aba:

bbabb b bbabbb

Critical pair: bbabbaba=abababbb.

Referenced by [19].

[7] babababa=abbbab

Overlap of [3] abbabbb=ba with [5] bbababa=abbbb:

abbabb b bbababa

Critical pair: abbabbabbbb=babababa.

Reduce LHS:

[3]	abb(abbabbb)b
	⇒ abbbab

Flip LHS and RHS.

Defines rule #6.

Referenced by [20].

[8] bbababbbb=abbaba

Overlap of [4] bbabbb=aba with [5] bbababa=abbbb:

bbab bb bbababa

Critical pair: bbababbbb=abaababa.

Reduce RHS:

[1]	ab(aa)baba
	⇒ abbaba

Defines rule #10.

[9] abbbba=bbabab

Overlap of [5] bbababa=abbbb with [1] aa=1:

bbabab a aa

Critical pair: bbabab=abbbba.

Flip LHS and RHS.

Referenced by [10], [11], [13], [16], [18].

[10] bbbba=abbabab

Overlap of [1] aa=1 with [9] abbbba=bbabab:

a a abbbba

Critical pair: abbabab=bbbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [12], [18].

[11] bbababbab=baba

Overlap of [3] abbabbb=ba with [9] abbbba=bbabab:

abb abbb abbbba

Critical pair: abbbbabab=baba.

Reduce LHS:

[9]	(abbbba)bab
	⇒ bbababbab

Referenced by [12].

[12] babba=ababb

Overlap of [3] abbabbb=ba with [10] bbbba=abbabab:

abbab bb bbbba

Critical pair: abbababbabab=babba.

Reduce LHS:

[11]	a(bbababbab)ab
[1]	⇒ abab(aa)b
	⇒ ababb

Flip LHS and RHS.

Defines rule #2.

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

[13] bbababbba=abbbababb

Overlap of [9] abbbba=bbabab with [12] babba=ababb:

abbb ba babba

Critical pair: abbbababb=bbababbba.

Flip LHS and RHS.

Referenced by [18].

[14] ababbbbb=bba

Overlap of [12] babba=ababb with [3] abbabbb=ba:

b abba abbabbb

Critical pair: bba=ababbbbb.

Flip LHS and RHS.

Referenced by [17].

[15] ababbbaba=bbbbb

Overlap of [12] babba=ababb with [5] bbababa=abbbb:

ba bba bbababa

Critical pair: baabbbb=ababbbaba.

Reduce LHS:

[1]	b(aa)bbbb
	⇒ bbbbb

Flip LHS and RHS.

Referenced by [18].

[16] abbbabab=babababb

Overlap of [12] babba=ababb with [12] babba=ababb:

bab ba babba

Critical pair: babababb=ababbbba.

Reduce RHS:

[9]	ab(abbbba)
	⇒ abbbabab

Flip LHS and RHS.

Referenced by [18].

[17] babbbbb=abba

Overlap of [1] aa=1 with [14] ababbbbb=bba:

a a ababbbbb

Critical pair: abba=babbbbb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [18].

[18] bbbbbbbbb=b

Overlap of [17] babbbbb=abba with [10] bbbba=abbabab:

babbbb b bbbba

Critical pair: babbbbabbabab=abbabbba.

Reduce LHS:

[9]	b(abbbba)bbabab
[13]	⇒ b(bbababbba)bab
[16]	⇒ b(abbbabab)bbab
[5]	⇒ (bbababa)bbbbab
[10]	⇒ abbbb(bbbba)b
[9]	⇒ (abbbba)bbababb
[13]	⇒ (bbababbba)babb
[16]	⇒ (abbbabab)bbabb
[9]	⇒ babab(abbbba)bb
[15]	⇒ b(ababbbaba)bbb
	⇒ bbbbbbbbb