Certificate for #24174 ⟨a, b | aa=a, babbbbb=a

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #3.

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

[2] babbbbb=a

Axiom: babbbbb=a.

Referenced by [3], [4], [6], [7], [8], [9], [10], [11], [16], [17], [18], [19].

[3] babbbba=abbbbb

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

babbbb b babbbbb

Critical pair: babbbba=aabbbbb.

Reduce RHS:

[1](aa)bbbbb
abbbbb

Referenced by [4], [5], [6], [7].

[4] abbbba=abbbbbbbbbb

Overlap of [2] babbbbb=a with [3] babbbba=abbbbb:

babbbb b babbbba

Critical pair: babbbbabbbbb=aabbbba.

Reduce LHS:

[3](babbbba)bbbbb
abbbbbbbbbb

Reduce RHS:

[1](aa)bbbba
abbbba

Flip LHS and RHS.

Referenced by [15].

[5] abbbbba=abbbbb

Overlap of [3] babbbba=abbbbb with [1] aa=a:

babbbb a aa

Critical pair: babbbba=abbbbba.

Reduce LHS:

[3](babbbba)
abbbbb

Flip LHS and RHS.

Referenced by [7].

[6] babba=abbbbbbbbba

Overlap of [3] babbbba=abbbbb with [3] babbbba=abbbbb:

babbb ba babbbba

Critical pair: babbbabbbbb=abbbbbbbbba.

Reduce LHS:

[2]babb(babbbbb)
babba

Referenced by [12].

[7] abbbbbbbbba=abbba

Overlap of [5] abbbbba=abbbbb with [3] babbbba=abbbbb:

abbbb ba babbbba

Critical pair: abbbbabbbbb=abbbbbbbbba.

Reduce LHS:

[2]abbb(babbbbb)
abbba

Flip LHS and RHS.

Referenced by [8], [12].

[8] abbbbbbbba=abba

Overlap of [7] abbbbbbbbba=abbba with [2] babbbbb=a:

abbbbbbbb ba babbbbb

Critical pair: abbbbbbbba=abbbabbbbb.

Reduce RHS:

[2]abb(babbbbb)
abba

Referenced by [9].

[9] abbbbbbba=aba

Overlap of [8] abbbbbbbba=abba with [2] babbbbb=a:

abbbbbbb ba babbbbb

Critical pair: abbbbbbba=abbabbbbb.

Reduce RHS:

[2]ab(babbbbb)
aba

Referenced by [10].

[10] baba=abba

Overlap of [2] babbbbb=a with [9] abbbbbbba=aba:

b abbbbb abbbbbbba

Critical pair: baba=abba.

Referenced by [11], [13].

[11] aba=ba

Overlap of [10] baba=abba with [2] babbbbb=a:

ba ba babbbbb

Critical pair: baa=abbabbbbb.

Reduce LHS:

[1]b(aa)
ba

Reduce RHS:

[2]ab(babbbbb)
aba

Flip LHS and RHS.

Referenced by [13], [14].

[12] babba=abbba

Simplify [6] babba=abbbbbbbbba.

Reduce RHS:

[7](abbbbbbbbba)
abbba

Referenced by [15].

[13] abba=bba

Overlap of [10] baba=abba with [11] aba=ba:

b aba aba

Critical pair: bba=abba.

Flip LHS and RHS.

Referenced by [14], [15].

[14] abbba=bbba

Overlap of [13] abba=bba with [11] aba=ba:

abb a aba

Critical pair: abbba=bbaba.

Reduce RHS:

[11]bb(aba)
bbba

Referenced by [15].

[15] bbbba=abbbbbbbbbb

Overlap of [13] abba=bba with [13] abba=bba:

abb a abba

Critical pair: abbbba=bbabba.

Reduce LHS:

[4](abbbba)
abbbbbbbbbb

Reduce RHS:

[12]b(babba)
[14]b(abbba)
bbbba

Flip LHS and RHS.

Referenced by [16].

[16] bbba=abbbbbbbbbbbbbbb

Overlap of [15] bbbba=abbbbbbbbbb with [2] babbbbb=a:

bbb ba babbbbb

Critical pair: bbba=abbbbbbbbbbbbbbb.

Referenced by [17].

[17] bba=abbbbbbbbbbbbbbbbbbbb

Overlap of [16] bbba=abbbbbbbbbbbbbbb with [2] babbbbb=a:

bb ba babbbbb

Critical pair: bba=abbbbbbbbbbbbbbbbbbbb.

Referenced by [18].

[18] ba=abbbbbbbbbbbbbbbbbbbbbbbbb

Overlap of [17] bba=abbbbbbbbbbbbbbbbbbbb with [2] babbbbb=a:

b ba babbbbb

Critical pair: ba=abbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #2.

Referenced by [19].

[19] abbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a

Overlap of [2] babbbbb=a with [18] ba=abbbbbbbbbbbbbbbbbbbbbbbbb:

babbbbb ba

Critical pair: abbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a.

Defines rule #1.