Certificate for #4211 ⟨a, b | aabbbbaba=ab

Completion settings:

[1] aabbbbaba=ab

Axiom: aabbbbaba=ab.

Referenced by [3].

[2] abbbb=c

Axiom: abbbb=c.

Defines rule #12.

Referenced by [3], [4], [10], [11], [12], [13], [16].

[3] acaba=ab

Overlap of [1] aabbbbaba=ab with [2] abbbb=c:

a abbbbaba abbbb

Critical pair: acaba=ab.

Defines rule #1.

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

[4] acabc=cb

Overlap of [3] acaba=ab with [2] abbbb=c:

acab a abbbb

Critical pair: acabc=abbbbb.

Reduce RHS:

[2](abbbb)b
cb

Defines rule #2.

Referenced by [6], [8], [9], [11], [14], [15], [17].

[5] abcaba=abb

Overlap of [3] acaba=ab with [3] acaba=ab:

acab a acaba

Critical pair: acabab=abcaba.

Reduce LHS:

[3](acaba)b
abb

Flip LHS and RHS.

Defines rule #4.

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

[6] cbb=abcabc

Overlap of [3] acaba=ab with [4] acabc=cb:

acab a acabc

Critical pair: acabcb=abcabc.

Reduce LHS:

[4](acabc)b
cbb

Defines rule #5.

Referenced by [13].

[7] abbcaba=abbb

Overlap of [3] acaba=ab with [5] abcaba=abb:

acab a abcaba

Critical pair: acababb=abbcaba.

Reduce LHS:

[3](acaba)bb
abbb

Flip LHS and RHS.

Defines rule #9.

[8] acabb=cbaba

Overlap of [4] acabc=cb with [5] abcaba=abb:

ac abc abcaba

Critical pair: acabb=cbaba.

Defines rule #7.

Referenced by [16].

[9] abcabcb=abbcabc

Overlap of [5] abcaba=abb with [4] acabc=cb:

abcab a acabc

Critical pair: abcabcb=abbcabc.

Defines rule #10.

Referenced by [13].

[10] abbbcaba=c

Overlap of [5] abcaba=abb with [5] abcaba=abb:

abcab a abcaba

Critical pair: abcababb=abbbcaba.

Reduce LHS:

[5](abcaba)bb
[2](abbbb)
c

Flip LHS and RHS.

Defines rule #13.

Referenced by [11], [12], [13], [14].

[11] ccaba=cb

Overlap of [3] acaba=ab with [10] abbbcaba=c:

acab a abbbcaba

Critical pair: acabc=abbbbcaba.

Reduce LHS:

[4](acabc)
cb

Reduce RHS:

[2](abbbb)caba
ccaba

Flip LHS and RHS.

Defines rule #3.

Referenced by [15].

[12] cbcaba=abcabc

Overlap of [5] abcaba=abb with [10] abbbcaba=c:

abcab a abbbcaba

Critical pair: abcabc=abbbbbcaba.

Reduce RHS:

[2](abbbb)bcaba
cbcaba

Flip LHS and RHS.

Defines rule #6.

Referenced by [17].

[13] abbcabcb=abbbcabc

Overlap of [10] abbbcaba=c with [2] abbbb=c:

abbbcab a abbbb

Critical pair: abbbcabc=cbbbb.

Reduce RHS:

[6](cbb)bb
[9](abcabcb)b
abbcabcb

Flip LHS and RHS.

Defines rule #14.

[14] abbbcabcb=ccabc

Overlap of [10] abbbcaba=c with [4] acabc=cb:

abbbcab a acabc

Critical pair: abbbcabcb=ccabc.

Defines rule #16.

[15] ccabcb=cbcabc

Overlap of [11] ccaba=cb with [4] acabc=cb:

ccab a acabc

Critical pair: ccabcb=cbcabc.

Defines rule #8.

[16] cbababb=acc

Overlap of [8] acabb=cbaba with [2] abbbb=c:

ac abb abbbb

Critical pair: acc=cbababb.

Flip LHS and RHS.

Defines rule #15.

[17] cbcabcb=abcabccabc

Overlap of [12] cbcaba=abcabc with [4] acabc=cb:

cbcab a acabc

Critical pair: cbcabcb=abcabccabc.

Defines rule #11.