Certificate for #1719 ⟨a, b | aabbabaab=a⟩

Completion settings:

Auxiliary generators:
1. c = ababa
2. d = ab
Reduction order:
- Right-to-left recursive path with deg(b) = deg(d) = 0, b < d; deg(c) = deg(a) = 1, c < a

[1] aabbabaab=a

Axiom: aabbabaab=a.

Referenced by [4].

[2] ababa=c

Axiom: ababa=c.

Referenced by [5].

[3] ab=d

Axiom: ab=d.

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

[4] adbdad=a

Overlap of [1] aabbabaab=a with [3] ab=d:

a abbabaab ab

Critical pair: adbabaab=a.

Reduce LHS:

[3]	adb(ab)aab
[3]	⇒ adbda(ab)
	⇒ adbdad

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

[5] dda=c

Overlap of [2] ababa=c with [3] ab=d:

ababa ab

Critical pair: daba=c.

Reduce LHS:

[3]	d(ab)a
	⇒ dda

Referenced by [6], [7], [8], [9], [10], [15], [18].

[6] cb=ddd

Overlap of [5] dda=c with [3] ab=d:

dd a ab

Critical pair: ddd=cb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [15], [23].

[7] adbda=cd

Overlap of [4] adbdad=a with [4] adbdad=a:

adbd ad adbdad

Critical pair: adbda=abdad.

Reduce RHS:

[3]	(ab)dad
[5]	⇒ (dda)d
	⇒ cd

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

[8] ada=cdc

Overlap of [4] adbdad=a with [5] dda=c:

adbda d dda

Critical pair: adbdac=ada.

Reduce LHS:

[7]	(adbda)c
	⇒ cdc

Flip LHS and RHS.

Referenced by [10], [11].

[9] cdbdad=c

Overlap of [5] dda=c with [4] adbdad=a:

dd a adbdad

Critical pair: dda=cdbdad.

Reduce LHS:

[5]	(dda)
	⇒ c

Flip LHS and RHS.

Referenced by [11], [15].

[10] cda=ddcdc

Overlap of [5] dda=c with [8] ada=cdc:

dd a ada

Critical pair: ddcdc=cda.

Flip LHS and RHS.

Referenced by [17].

[11] cdbdcdc=ca

Overlap of [9] cdbdad=c with [8] ada=cdc:

cdbd ad ada

Critical pair: cdbdcdc=ca.

Referenced by [19].

[12] a=cdd

Overlap of [4] adbdad=a with [7] adbda=cd:

adbdad adbda

Critical pair: cdd=a.

Flip LHS and RHS.

Defines rule #6.

Referenced by [13], [14], [16], [17], [18], [19].

[13] cddbdcdd=cdddbdcd

Overlap of [4] adbdad=a with [7] adbda=cd:

adbd ad adbda

Critical pair: adbdcd=abda.

Reduce LHS:

[12]	(a)dbdcd
	⇒ cdddbdcd

Reduce RHS:

[12]	(a)bda
[12]	⇒ cddbd(a)
	⇒ cddbdcdd

Flip LHS and RHS.

Referenced by [21].

[14] cdddbdd=cdb

Overlap of [7] adbda=cd with [3] ab=d:

adbd a ab

Critical pair: adbdd=cdb.

Reduce LHS:

[12]	(a)dbdd
	⇒ cdddbdd

Defines rule #5.

Referenced by [25].

[15] cdbdcd=ddc

Overlap of [9] cdbdad=c with [7] adbda=cd:

cdbd ad adbda

Critical pair: cdbdcd=cbda.

Reduce RHS:

[6]	(cb)da
[5]	⇒ dd(dda)
	⇒ ddc

Referenced by [20], [22], [23].

[16] cddb=d

Overlap of [3] ab=d with [12] a=cdd:

ab a

Critical pair: cddb=d.

Defines rule #3.

Referenced by [21], [22], [24].

[17] cdcdd=ddcdc

Simplify [10] cda=ddcdc.

Reduce LHS:

[12]	cd(a)
	⇒ cdcdd

Defines rule #10.

[18] ddcdd=c

Overlap of [5] dda=c with [12] a=cdd:

dd a a

Critical pair: ddcdd=c.

Defines rule #2.

Referenced by [21], [23], [25].

[19] cdbdcdc=ccdd

Simplify [11] cdbdcdc=ca.

Reduce RHS:

[12]	c(a)
	⇒ ccdd

Referenced by [20].

[20] ccdd=ddcc

Overlap of [19] cdbdcdc=ccdd with [15] cdbdcd=ddc:

cdbdcdc cdbdcd

Critical pair: ddcc=ccdd.

Flip LHS and RHS.

Defines rule #9.

[21] cdddbdcd=c

Overlap of [13] cddbdcdd=cdddbdcd with [16] cddb=d:

cddbdcdd cddb

Critical pair: ddcdd=cdddbdcd.

Reduce LHS:

[18]	(ddcdd)
	⇒ c

Flip LHS and RHS.

Referenced by [23], [24].

[22] cdbdd=ddcdb

Overlap of [15] cdbdcd=ddc with [16] cddb=d:

cdbd cd cddb

Critical pair: cdbdd=ddcdb.

Defines rule #4.

[23] cdbdc=ddddcd

Overlap of [15] cdbdcd=ddc with [21] cdddbdcd=c:

cdbd cd cdddbdcd

Critical pair: cdbdc=ddcddbdcd.

Reduce RHS:

[18]	(ddcdd)bdcd
[6]	⇒ (cb)dcd
	⇒ ddddcd

Defines rule #7.

[24] cdddbdc=ddcd

Overlap of [21] cdddbdcd=c with [21] cdddbdcd=c:

cdddbd cd cdddbdcd

Critical pair: cdddbdc=cddbdcd.

Reduce RHS:

[16]	(cddb)dcd
	⇒ ddcd

Defines rule #8.

[25] cdbcdd=cdddbc

Overlap of [14] cdddbdd=cdb with [18] ddcdd=c:

cdddb dd ddcdd

Critical pair: cdddbc=cdbcdd.

Flip LHS and RHS.

Defines rule #11.