Certificate for #4195 ⟨a, b | aabbbaaba=ab⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1
Auxiliary generators:
1. abbb=c

[1] aabbbaaba=ab

Axiom: aabbbaaba=ab.

Referenced by [3].

[2] abbb=c

Axiom: abbb=c.

Defines rule #9.

Referenced by [3], [4], [7], [10], [12], [14].

[3] acaaba=ab

Overlap of [1] aabbbaaba=ab with [2] abbb=c:

a abbbaaba abbb

Critical pair: acaaba=ab.

Defines rule #1.

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

[4] acaabc=cb

Overlap of [3] acaaba=ab with [2] abbb=c:

acaab a abbb

Critical pair: acaabc=abbbb.

Reduce RHS:

[2]	(abbb)b
	⇒ cb

Defines rule #2.

Referenced by [6], [8], [9], [11], [13], [15].

[5] abcaaba=abb

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

acaab a acaaba

Critical pair: acaabab=abcaaba.

Reduce LHS:

[3]	(acaaba)b
	⇒ abb

Flip LHS and RHS.

Defines rule #4.

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

[6] cbb=abcaabc

Overlap of [3] acaaba=ab with [4] acaabc=cb:

acaab a acaabc

Critical pair: acaabcb=abcaabc.

Reduce LHS:

[4]	(acaabc)b
	⇒ cbb

Defines rule #5.

Referenced by [11], [12].

[7] abbcaaba=c

Overlap of [3] acaaba=ab with [5] abcaaba=abb:

acaab a abcaaba

Critical pair: acaababb=abbcaaba.

Reduce LHS:

[3]	(acaaba)bb
[2]	⇒ (abbb)
	⇒ c

Flip LHS and RHS.

Defines rule #10.

[8] acaabb=cbaaba

Overlap of [4] acaabc=cb with [5] abcaaba=abb:

aca abc abcaaba

Critical pair: acaabb=cbaaba.

Defines rule #7.

Referenced by [14].

[9] abcaabcb=abbcaabc

Overlap of [5] abcaaba=abb with [4] acaabc=cb:

abcaab a acaabc

Critical pair: abcaabcb=abbcaabc.

Defines rule #11.

Referenced by [12].

[10] ccaaba=cb

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

abcaab a abcaaba

Critical pair: abcaababb=abbbcaaba.

Reduce LHS:

[5]	(abcaaba)bb
[2]	⇒ (abbb)b
	⇒ cb

Reduce RHS:

[2]	(abbb)caaba
	⇒ ccaaba

Flip LHS and RHS.

Defines rule #3.

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

[11] cbcaaba=abcaabc

Overlap of [4] acaabc=cb with [10] ccaaba=cb:

acaab c ccaaba

Critical pair: acaabcb=cbcaaba.

Reduce LHS:

[4]	(acaabc)b
[6]	⇒ (cbb)
	⇒ abcaabc

Flip LHS and RHS.

Defines rule #6.

Referenced by [15].

[12] abbcaabcb=ccaabc

Overlap of [10] ccaaba=cb with [2] abbb=c:

ccaab a abbb

Critical pair: ccaabc=cbbbb.

Reduce RHS:

[6]	(cbb)bb
[9]	⇒ (abcaabcb)b
	⇒ abbcaabcb

Flip LHS and RHS.

Defines rule #14.

[13] ccaabcb=cbcaabc

Overlap of [10] ccaaba=cb with [4] acaabc=cb:

ccaab a acaabc

Critical pair: ccaabcb=cbcaabc.

Defines rule #8.

[14] cbaabab=acac

Overlap of [8] acaabb=cbaaba with [2] abbb=c:

aca abb abbb

Critical pair: acac=cbaabab.

Flip LHS and RHS.

Defines rule #12.

[15] cbcaabcb=abcaabccaabc

Overlap of [11] cbcaaba=abcaabc with [4] acaabc=cb:

cbcaab a acaabc

Critical pair: cbcaabcb=abcaabccaabc.

Defines rule #13.