Certificate for #21200 ⟨a, b | aaa=1, ababbbbb=1⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

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

[2] ababbbbb=1

Axiom: ababbbbb=1.

Referenced by [3], [6], [7], [8], [9], [18], [20], [22].

[3] aa=babbbbb

Overlap of [1] aaa=1 with [2] ababbbbb=1:

aa a ababbbbb

Critical pair: aa=babbbbb.

Defines rule #3.

Referenced by [4], [10], [11], [13], [14], [15].

[4] babbbbba=1

Overlap of [1] aaa=1 with [3] aa=babbbbb:

aaa aa

Critical pair: babbbbba=1.

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

[5] bbbbba=babbbb

Overlap of [4] babbbbba=1 with [4] babbbbba=1:

babbbb ba babbbbba

Critical pair: babbbb=bbbbba.

Flip LHS and RHS.

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

[6] abababbbb=a

Overlap of [2] ababbbbb=1 with [5] bbbbba=babbbb:

aba bbbbb bbbbba

Critical pair: abababbbb=a.

Referenced by [10].

[7] ababbabbbb=ba

Overlap of [2] ababbbbb=1 with [5] bbbbba=babbbb:

abab bbbb bbbbba

Critical pair: ababbabbbb=ba.

Referenced by [12].

[8] ababbbbabbbb=bbba

Overlap of [2] ababbbbb=1 with [5] bbbbba=babbbb:

ababbb bb bbbbba

Critical pair: ababbbbabbbb=bbba.

Referenced by [13].

[9] bbbba=abbbb

Overlap of [2] ababbbbb=1 with [5] bbbbba=babbbb:

ababbbb b bbbbba

Critical pair: ababbbbbabbbb=bbbba.

Reduce LHS:

[2](ababbbbb)abbbb
abbbb

Flip LHS and RHS.

Defines rule #2.

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

[10] bababbbb=1

Overlap of [1] aaa=1 with [6] abababbbb=a:

aa a abababbbb

Critical pair: aaa=bababbbb.

Reduce LHS:

[3](aa)a
[4](babbbbba)
⇒ 1

Flip LHS and RHS.

Referenced by [11].

[11] babbabbbbbbbbb=a

Overlap of [10] bababbbb=1 with [9] bbbba=abbbb:

baba bbbb bbbba

Critical pair: babaabbbb=a.

Reduce LHS:

[3]bab(aa)bbbb
babbabbbbbbbbb

Referenced by [14], [18], [19].

[12] baba=abab

Overlap of [7] ababbabbbb=ba with [4] babbbbba=1:

abab babbbb babbbbba

Critical pair: abab=baba.

Flip LHS and RHS.

Referenced by [18].

[13] abbabbbbbbbbbbbbb=bbba

Overlap of [8] ababbbbabbbb=bbba with [9] bbbba=abbbb:

aba bbbbabbbb bbbba

Critical pair: abaabbbbbbbb=bbba.

Reduce LHS:

[3]ab(aa)bbbbbbbb
abbabbbbbbbbbbbbb

Referenced by [15], [21].

[14] babbbabbbbbbbbbbbbbbbbb=abbba

Overlap of [11] babbabbbbbbbbb=a with [9] bbbba=abbbb:

babbabbbbbbbb b bbbba

Critical pair: babbabbbbbbbbabbbb=abbba.

Reduce LHS:

[9]babbabbbb(bbbba)bbbb
[9]babba(bbbba)bbbbbbbb
[3]babb(aa)bbbbbbbbbbbb
babbbabbbbbbbbbbbbbbbbb

Referenced by [16], [17].

[15] bbbabbba=abbbabbbbbbbbbbbbbbbbbbbbb

Overlap of [13] abbabbbbbbbbbbbbb=bbba with [9] bbbba=abbbb:

abbabbbbbbbbbbbb b bbbba

Critical pair: abbabbbbbbbbbbbbabbbb=bbbabbba.

Reduce LHS:

[9]abbabbbbbbbb(bbbba)bbbb
[9]abbabbbb(bbbba)bbbbbbbb
[9]abba(bbbba)bbbbbbbbbbbb
[3]abb(aa)bbbbbbbbbbbbbbbb
abbbabbbbbbbbbbbbbbbbbbbbb

Flip LHS and RHS.

Referenced by [16].

[16] bbabbba=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Overlap of [15] bbbabbba=abbbabbbbbbbbbbbbbbbbbbbbb with [14] babbbabbbbbbbbbbbbbbbbb=abbba:

bb babbba babbbabbbbbbbbbbbbbbbbb

Critical pair: bbabbba=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Referenced by [17].

[17] babbba=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Overlap of [16] bbabbba=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [14] babbbabbbbbbbbbbbbbbbbb=abbba:

b babbba babbbabbbbbbbbbbbbbbbbb

Critical pair: babbba=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #6.

Referenced by [18].

[18] babba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Overlap of [17] babbba=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [11] babbabbbbbbbbb=a:

babb ba babbabbbbbbbbb

Critical pair: babba=abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbabbbbbbbbb.

Reduce RHS:

[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbbbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbabbbbb(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[9]abbbab(bbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[12]abb(baba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[12]ab(baba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[12]a(baba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]a(ababbbbb)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Referenced by [19].

[19] abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a

Overlap of [11] babbabbbbbbbbb=a with [18] babba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb:

babbabbbbbbbbb babba

Critical pair: abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a.

Referenced by [20], [21].

[20] aba=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Overlap of [2] ababbbbb=1 with [19] abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a:

ab abbbbb abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Critical pair: aba=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #4.

Referenced by [22].

[21] abba=bbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Overlap of [13] abbabbbbbbbbbbbbb=bbba with [19] abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a:

abb abbbbbbbbbbbbb abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Critical pair: abba=bbbabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #5.

[22] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=1

Overlap of [2] ababbbbb=1 with [20] aba=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb:

ababbbbb aba

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=1.

Defines rule #1.