Certificate for #331 ⟨a, b | abababba=1⟩

Completion settings:

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

[1] abababba=1

Axiom: abababba=1.

Referenced by [4].

[2] ba=c

Axiom: ba=c.

Defines rule #7.

Referenced by [4], [5], [7], [12], [22].

[3] bca=d

Axiom: bca=d.

Referenced by [6], [22].

[4] accbc=1

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

a bababba ba

Critical pair: acbabba=1.

Reduce LHS:

[2]	ac(ba)bba
[2]	⇒ accb(ba)
	⇒ accbc

Referenced by [5], [6], [8], [9], [10], [11], [13].

[5] cccbc=b

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

b a accbc

Critical pair: b=cccbc.

Flip LHS and RHS.

Referenced by [10].

[6] accd=a

Overlap of [4] accbc=1 with [3] bca=d:

acc bc bca

Critical pair: accd=a.

Referenced by [7].

[7] cccd=c

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

b a accd

Critical pair: ba=cccd.

Reduce LHS:

[2]	(ba)
	⇒ c

Flip LHS and RHS.

Referenced by [8].

[8] ccd=1

Overlap of [4] accbc=1 with [7] cccd=c:

accb c cccd

Critical pair: accbc=ccd.

Reduce LHS:

[4]	(accbc)
	⇒ 1

Flip LHS and RHS.

Defines rule #2.

Referenced by [9], [14], [15], [16], [17], [18], [19], [20], [23], [24].

[9] accb=cd

Overlap of [4] accbc=1 with [8] ccd=1:

accb c ccd

Critical pair: accb=cd.

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

[10] ccbc=cdb

Overlap of [4] accbc=1 with [5] cccbc=b:

accb c cccbc

Critical pair: accbb=ccbc.

Reduce LHS:

[9]	(accb)b
	⇒ cdb

Flip LHS and RHS.

Referenced by [18].

[11] cdc=1

Overlap of [4] accbc=1 with [9] accb=cd:

accbc accb

Critical pair: cdc=1.

Referenced by [13].

[12] accc=cda

Overlap of [9] accb=cd with [2] ba=c:

acc b ba

Critical pair: accc=cda.

Referenced by [14].

[13] dc=cd

Overlap of [4] accbc=1 with [11] cdc=1:

accb c cdc

Critical pair: accb=dc.

Reduce LHS:

[9]	(accb)
	⇒ cd

Flip LHS and RHS.

Defines rule #1.

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

[14] ac=cdad

Overlap of [12] accc=cda with [8] ccd=1:

ac cc ccd

Critical pair: ac=cdad.

Defines rule #3.

Referenced by [15], [16].

[15] daddb=cd

Overlap of [9] accb=cd with [14] ac=cdad:

accb ac

Critical pair: cdadcb=cd.

Reduce LHS:

[13]	cda(dc)b
[14]	⇒ cd(ac)db
[13]	⇒ c(dc)daddb
[8]	⇒ (ccd)daddb
	⇒ daddb

Referenced by [23].

[16] daddd=a

Overlap of [14] ac=cdad with [8] ccd=1:

a c ccd

Critical pair: a=cdadcd.

Reduce RHS:

[13]	cda(dc)d
[14]	⇒ cd(ac)dd
[13]	⇒ c(dc)daddd
[8]	⇒ (ccd)daddd
	⇒ daddd

Flip LHS and RHS.

Referenced by [17], [21].

[17] addd=cca

Overlap of [8] ccd=1 with [16] daddd=a:

cc d daddd

Critical pair: cca=addd.

Flip LHS and RHS.

Defines rule #4.

[18] bc=cddb

Overlap of [13] dc=cd with [10] ccbc=cdb:

d c ccbc

Critical pair: dcdb=cdcbc.

Reduce LHS:

[13]	(dc)db
	⇒ cddb

Reduce RHS:

[13]	c(dc)bc
[8]	⇒ (ccd)bc
	⇒ bc

Flip LHS and RHS.

Defines rule #6.

Referenced by [19], [22].

[19] dddbd=b

Overlap of [18] bc=cddb with [8] ccd=1:

b c ccd

Critical pair: b=cddbcd.

Reduce RHS:

[18]	cdd(bc)d
[13]	⇒ cd(dc)ddbd
[13]	⇒ c(dc)dddbd
[8]	⇒ (ccd)dddbd
	⇒ dddbd

Flip LHS and RHS.

Referenced by [20], [21].

[20] ddbd=ccb

Overlap of [8] ccd=1 with [19] dddbd=b:

cc d dddbd

Critical pair: ccb=ddbd.

Flip LHS and RHS.

Referenced by [22].

[21] abd=dab

Overlap of [16] daddd=a with [19] dddbd=b:

da ddd dddbd

Critical pair: dab=abd.

Flip LHS and RHS.

Referenced by [22].

[22] dbd=ccccb

Overlap of [3] bca=d with [21] abd=dab:

bc a abd

Critical pair: bcdab=dbd.

Reduce LHS:

[18]	(bc)dab
[20]	⇒ c(ddbd)ab
[2]	⇒ ccc(ba)b
	⇒ ccccb

Flip LHS and RHS.

Referenced by [24].

[23] addb=c

Overlap of [8] ccd=1 with [15] daddb=cd:

cc d daddb

Critical pair: cccd=addb.

Reduce LHS:

[8]	c(ccd)
	⇒ c

Flip LHS and RHS.

Defines rule #8.

[24] bd=ccccccb

Overlap of [8] ccd=1 with [22] dbd=ccccb:

cc d dbd

Critical pair: ccccccb=bd.

Flip LHS and RHS.

Defines rule #5.