Certificate for #5341 ⟨a, b | ababaab=aaba⟩

Completion settings:

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

[1] ababaab=aaba

Axiom: ababaab=aaba.

Referenced by [4].

[2] aba=c

Axiom: aba=c.

Defines rule #17.

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

[3] bca=d

Axiom: bca=d.

Defines rule #11.

Referenced by [7], [8], [10], [11], [13], [15].

[4] ababaab=ac

Simplify [1] ababaab=aaba.

Reduce RHS:

[2]	a(aba)
	⇒ ac

Referenced by [5].

[5] cbaab=ac

Overlap of [4] ababaab=ac with [2] aba=c:

ababaab aba

Critical pair: cbaab=ac.

Referenced by [8].

[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 #10.

Referenced by [8].

[7] dba=bcc

Overlap of [3] bca=d with [2] aba=c:

bc a aba

Critical pair: bcc=dba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [12], [14], [16].

[8] adb=ac

Simplify [5] cbaab=ac.

Reduce LHS:

[6]	(cba)ab
[3]	⇒ a(bca)b
	⇒ adb

Defines rule #7.

Referenced by [9], [10], [11], [12].

[9] cdb=cc

Overlap of [2] aba=c with [8] adb=ac:

ab a adb

Critical pair: abac=cdb.

Reduce LHS:

[2]	(aba)c
	⇒ cc

Flip LHS and RHS.

Defines rule #1.

Referenced by [13], [14].

[10] ddb=dc

Overlap of [3] bca=d with [8] adb=ac:

bc a adb

Critical pair: bcac=ddb.

Reduce LHS:

[3]	(bca)c
	⇒ dc

Flip LHS and RHS.

Defines rule #2.

Referenced by [15], [16], [18], [21], [23].

[11] acca=add

Overlap of [8] adb=ac with [3] bca=d:

ad b bca

Critical pair: add=acca.

Flip LHS and RHS.

Referenced by [20].

[12] aca=abcc

Overlap of [8] adb=ac with [7] dba=bcc:

a db dba

Critical pair: abcc=aca.

Flip LHS and RHS.

Defines rule #18.

[13] ccca=cdd

Overlap of [9] cdb=cc with [3] bca=d:

cd b bca

Critical pair: cdd=ccca.

Flip LHS and RHS.

Referenced by [17].

[14] cca=cbcc

Overlap of [9] cdb=cc with [7] dba=bcc:

c db dba

Critical pair: cbcc=cca.

Flip LHS and RHS.

Defines rule #13.

Referenced by [15], [17], [19], [20], [22], [24].

[15] dcbcc=ddd

Overlap of [10] ddb=dc with [3] bca=d:

dd b bca

Critical pair: ddd=dcca.

Reduce RHS:

[14]	d(cca)
	⇒ dcbcc

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [22].

[16] dca=dbcc

Overlap of [10] ddb=dc with [7] dba=bcc:

d db dba

Critical pair: dbcc=dca.

Flip LHS and RHS.

Defines rule #14.

[17] ccbcc=cdd

Simplify [13] ccca=cdd.

Reduce LHS:

[14]	c(cca)
	⇒ ccbcc

Defines rule #3.

Referenced by [18], [19], [21], [23].

[18] cdccc=ccbcdd

Overlap of [17] ccbcc=cdd with [17] ccbcc=cdd:

ccb cc ccbcc

Critical pair: ccbcdd=cddbcc.

Reduce RHS:

[10]	c(ddb)cc
	⇒ cdccc

Flip LHS and RHS.

Defines rule #5.

[19] cdda=ccbcbcc

Overlap of [17] ccbcc=cdd with [14] cca=cbcc:

ccb cc cca

Critical pair: ccbcbcc=cdda.

Flip LHS and RHS.

Defines rule #15.

[20] acbcc=add

Overlap of [11] acca=add with [14] cca=cbcc:

a cca cca

Critical pair: acbcc=add.

Defines rule #8.

Referenced by [23], [24].

[21] ddccc=dcbcdd

Overlap of [15] dcbcc=ddd with [17] ccbcc=cdd:

dcb cc ccbcc

Critical pair: dcbcdd=dddbcc.

Reduce RHS:

[10]	d(ddb)cc
	⇒ ddccc

Flip LHS and RHS.

Defines rule #6.

[22] ddda=dcbcbcc

Overlap of [15] dcbcc=ddd with [14] cca=cbcc:

dcb cc cca

Critical pair: dcbcbcc=ddda.

Flip LHS and RHS.

Defines rule #16.

[23] adccc=acbcdd

Overlap of [20] acbcc=add with [17] ccbcc=cdd:

acb cc ccbcc

Critical pair: acbcdd=addbcc.

Reduce RHS:

[10]	a(ddb)cc
	⇒ adccc

Flip LHS and RHS.

Defines rule #9.

[24] adda=acbcbcc

Overlap of [20] acbcc=add with [14] cca=cbcc:

acb cc cca

Critical pair: acbcbcc=adda.

Flip LHS and RHS.

Defines rule #19.