Certificate for #3079 ⟨a, b | aababbabaab=1⟩

Completion settings:

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

[1] aababbabaab=1

Axiom: aababbabaab=1.

Referenced by [4].

[2] aba=c

Axiom: aba=c.

Defines rule #8.

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

[3] ccc=d

Axiom: ccc=d.

Defines rule #5.

Referenced by [5], [11].

[4] acbbcab=1

Overlap of [1] aababbabaab=1 with [2] aba=c:

a ababbabaab aba

Critical pair: acbbabaab=1.

Reduce LHS:

[2]	acbb(aba)ab
	⇒ acbbcab

Referenced by [7], [10].

[5] cd=dc

Overlap of [3] ccc=d with [3] ccc=d:

c cc ccc

Critical pair: cd=dc.

Defines rule #2.

Referenced by [17], [18].

[6] cba=abc

Overlap of [2] aba=c with [2] aba=c:

ab a aba

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #6.

[7] acbbcc=a

Overlap of [4] acbbcab=1 with [2] aba=c:

acbbc ab aba

Critical pair: acbbcc=a.

Referenced by [8], [9], [11].

[8] ccbbcc=c

Overlap of [2] aba=c with [7] acbbcc=a:

ab a acbbcc

Critical pair: aba=ccbbcc.

Reduce LHS:

[2]	(aba)
	⇒ c

Flip LHS and RHS.

Referenced by [9].

[9] acbbc=abbcc

Overlap of [7] acbbcc=a with [8] ccbbcc=c:

acbb cc ccbbcc

Critical pair: acbbc=abbcc.

Referenced by [10], [11].

[10] abbccab=1

Overlap of [4] acbbcab=1 with [9] acbbc=abbcc:

acbbcab acbbc

Critical pair: abbccab=1.

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

[11] abbd=a

Overlap of [7] acbbcc=a with [9] acbbc=abbcc:

acbbcc acbbc

Critical pair: abbccc=a.

Reduce LHS:

[3]	abb(ccc)
	⇒ abbd

Referenced by [12].

[12] abbcca=bd

Overlap of [10] abbccab=1 with [11] abbd=a:

abbcc ab abbd

Critical pair: abbcca=bd.

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

[13] bdb=1

Overlap of [10] abbccab=1 with [12] abbcca=bd:

abbccab abbcca

Critical pair: bdb=1.

Referenced by [15], [16].

[14] bcca=abbccbd

Overlap of [10] abbccab=1 with [12] abbcca=bd:

abbcc ab abbcca

Critical pair: abbccbd=bcca.

Flip LHS and RHS.

Referenced by [18].

[15] bd=db

Overlap of [10] abbccab=1 with [13] bdb=1:

abbcca b bdb

Critical pair: abbcca=db.

Reduce LHS:

[12]	(abbcca)
	⇒ bd

Defines rule #1.

Referenced by [16], [18], [19], [20].

[16] dbb=1

Overlap of [13] bdb=1 with [15] bd=db:

bdb bd

Critical pair: dbb=1.

Defines rule #3.

Referenced by [17], [18], [20], [21].

[17] dcbb=c

Overlap of [5] cd=dc with [16] dbb=1:

c d dbb

Critical pair: c=dcbb.

Flip LHS and RHS.

Referenced by [19].

[18] bcca=accb

Simplify [14] bcca=abbccbd.

Reduce RHS:

[15]	abbcc(bd)
[5]	⇒ abbc(cd)b
[5]	⇒ abb(cd)cb
[15]	⇒ ab(bd)ccb
[15]	⇒ a(bd)bccb
[16]	⇒ a(dbb)ccb
	⇒ accb

Referenced by [21].

[19] dbcbb=bc

Overlap of [15] bd=db with [17] dcbb=c:

b d dcbb

Critical pair: bc=dbcbb.

Flip LHS and RHS.

Referenced by [20].

[20] cbb=bbc

Overlap of [15] bd=db with [19] dbcbb=bc:

b d dbcbb

Critical pair: bbc=dbbcbb.

Reduce RHS:

[16]	(dbb)cbb
	⇒ cbb

Flip LHS and RHS.

Defines rule #4.

[21] cca=dbaccb

Overlap of [16] dbb=1 with [18] bcca=accb:

db b bcca

Critical pair: dbaccb=cca.

Flip LHS and RHS.

Defines rule #7.