Certificate for #1533 ⟨a, b | abbaabbaab=1⟩

Completion settings:

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

[1] abbaabbaab=1

Axiom: abbaabbaab=1.

Referenced by [4].

[2] ba=c

Axiom: ba=c.

Defines rule #10.

Referenced by [4], [5], [8], [9], [10], [11], [12], [16], [20], [21].

[3] bcca=d

Axiom: bcca=d.

Referenced by [6], [8], [10], [13], [14], [15].

[4] abcabcab=1

Overlap of [1] abbaabbaab=1 with [2] ba=c:

ab baabbaab ba

Critical pair: abcabbaab=1.

Reduce LHS:

[2]	abcab(ba)ab
	⇒ abcabcab

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

[5] abcabcac=a

Overlap of [4] abcabcab=1 with [2] ba=c:

abcabca b ba

Critical pair: abcabcac=a.

Referenced by [14].

[6] abcabcad=cca

Overlap of [4] abcabcab=1 with [3] bcca=d:

abcabca b bcca

Critical pair: abcabcad=cca.

Referenced by [15].

[7] cab=abc

Overlap of [4] abcabcab=1 with [4] abcabcab=1:

abc abcab abcabcab

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #8.

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

[8] db=cbcc

Overlap of [3] bcca=d with [7] cab=abc:

bc ca cab

Critical pair: bcabc=db.

Reduce LHS:

[7]	b(cab)c
[2]	⇒ (ba)bcc
	⇒ cbcc

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [13].

[9] abca=cac

Overlap of [7] cab=abc with [2] ba=c:

ca b ba

Critical pair: cac=abca.

Flip LHS and RHS.

Defines rule #12.

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

[10] dc=cd

Overlap of [8] db=cbcc with [2] ba=c:

d b ba

Critical pair: dc=cbcca.

Reduce RHS:

[3]	c(bcca)
	⇒ cd

Defines rule #1.

Referenced by [14], [18], [19].

[11] cbca=bcac

Overlap of [2] ba=c with [9] abca=cac:

b a abca

Critical pair: bcac=cbca.

Flip LHS and RHS.

Defines rule #11.

[12] cacb=acbc

Overlap of [9] abca=cac with [7] cab=abc:

ab ca cab

Critical pair: ababc=cacb.

Reduce LHS:

[2]	a(ba)bc
	⇒ acbc

Flip LHS and RHS.

Defines rule #9.

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

[13] accbcc=1

Overlap of [4] abcabcab=1 with [9] abca=cac:

abcabcab abca

Critical pair: cacbcab=1.

Reduce LHS:

[12]	(cacb)cab
[3]	⇒ ac(bcca)b
[8]	⇒ ac(db)
	⇒ accbcc

Referenced by [17], [18].

[14] accd=a

Overlap of [5] abcabcac=a with [9] abca=cac:

abcabcac abca

Critical pair: cacbcac=a.

Reduce LHS:

[12]	(cacb)cac
[3]	⇒ ac(bcca)c
[10]	⇒ ac(dc)
	⇒ accd

Referenced by [16].

[15] cca=acdd

Overlap of [6] abcabcad=cca with [9] abca=cac:

abcabcad abca

Critical pair: cacbcad=cca.

Reduce LHS:

[12]	(cacb)cad
[3]	⇒ ac(bcca)d
	⇒ acdd

Flip LHS and RHS.

Defines rule #4.

[16] cccd=c

Overlap of [2] ba=c with [14] accd=a:

b a accd

Critical pair: ba=cccd.

Reduce LHS:

[2]	(ba)
	⇒ c

Flip LHS and RHS.

Referenced by [17].

[17] accbc=cd

Overlap of [13] accbcc=1 with [16] cccd=c:

accb cc cccd

Critical pair: accbc=cd.

Referenced by [18], [19].

[18] ccd=1

Overlap of [13] accbcc=1 with [17] accbc=cd:

accbcc accbc

Critical pair: cdc=1.

Reduce LHS:

[10]	c(dc)
	⇒ ccd

Defines rule #2.

Referenced by [19].

[19] accb=d

Overlap of [17] accbc=cd with [18] ccd=1:

accb c ccd

Critical pair: accb=cdcd.

Reduce RHS:

[10]	c(dc)d
[18]	⇒ (ccd)d
	⇒ d

Defines rule #7.

Referenced by [20], [21].

[20] cccb=bd

Overlap of [2] ba=c with [19] accb=d:

b a accb

Critical pair: bd=cccb.

Flip LHS and RHS.

Defines rule #6.

[21] da=accc

Overlap of [19] accb=d with [2] ba=c:

acc b ba

Critical pair: accc=da.

Flip LHS and RHS.

Defines rule #3.