Certificate for #5196 ⟨a, b | aababba=abab⟩

Completion settings:

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

[1] aababba=abab

Axiom: aababba=abab.

Referenced by [5].

[2] ab=c

Axiom: ab=c.

Defines rule #6.

Referenced by [5], [6], [8], [13], [15], [18].

[3] cc=d

Axiom: cc=d.

Defines rule #2.

Referenced by [5], [6], [7], [10], [12], [19].

[4] dbdb=e

Axiom: dbdb=e.

Defines rule #16.

Referenced by [11], [13], [16], [17], [18].

[5] aababba=d

Simplify [1] aababba=abab.

Reduce RHS:

[2]	(ab)ab
[2]	⇒ c(ab)
[3]	⇒ (cc)
	⇒ d

Referenced by [6].

[6] adba=d

Overlap of [5] aababba=d with [2] ab=c:

a ababba ab

Critical pair: acabba=d.

Reduce LHS:

[2]	ac(ab)ba
[3]	⇒ a(cc)ba
	⇒ adba

Defines rule #7.

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

[7] dc=cd

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

c c cc

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #1.

[8] adbc=db

Overlap of [6] adba=d with [2] ab=c:

adb a ab

Critical pair: adbc=db.

Referenced by [10], [14].

[9] adbd=ddba

Overlap of [6] adba=d with [6] adba=d:

adb a adba

Critical pair: adbd=ddba.

Defines rule #10.

Referenced by [10], [13].

[10] dbc=ddba

Overlap of [8] adbc=db with [3] cc=d:

adb c cc

Critical pair: adbd=dbc.

Reduce LHS:

[9]	(adbd)
	⇒ ddba

Flip LHS and RHS.

Defines rule #12.

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

[11] dbddba=ec

Overlap of [4] dbdb=e with [10] dbc=ddba:

db db dbc

Critical pair: dbddba=ec.

Referenced by [21].

[12] ddbac=dbd

Overlap of [10] dbc=ddba with [3] cc=d:

db c cc

Critical pair: dbd=ddbac.

Flip LHS and RHS.

Defines rule #13.

Referenced by [20].

[13] dddba=ae

Overlap of [9] adbd=ddba with [4] dbdb=e:

a dbd dbdb

Critical pair: ae=ddbab.

Reduce RHS:

[2]	ddb(ab)
[10]	⇒ d(dbc)
	⇒ dddba

Flip LHS and RHS.

Defines rule #9.

Referenced by [15], [20].

[14] addba=db

Overlap of [8] adbc=db with [10] dbc=ddba:

a dbc dbc

Critical pair: addba=db.

Defines rule #8.

Referenced by [15], [16].

[15] dbb=aae

Overlap of [14] addba=db with [2] ab=c:

addb a ab

Critical pair: addbc=dbb.

Reduce LHS:

[10]	ad(dbc)
[13]	⇒ a(dddba)
	⇒ aae

Flip LHS and RHS.

Defines rule #15.

Referenced by [17].

[16] addbd=ea

Overlap of [14] addba=db with [6] adba=d:

addb a adba

Critical pair: addbd=dbdba.

Reduce RHS:

[4]	(dbdb)a
	⇒ ea

Referenced by [18], [22].

[17] eb=dbaae

Overlap of [4] dbdb=e with [15] dbb=aae:

db db dbb

Critical pair: dbaae=eb.

Flip LHS and RHS.

Defines rule #14.

[18] ec=ade

Overlap of [16] addbd=ea with [4] dbdb=e:

ad dbd dbdb

Critical pair: ade=eab.

Reduce RHS:

[2]	e(ab)
	⇒ ec

Flip LHS and RHS.

Defines rule #5.

Referenced by [19], [20], [21].

[19] ed=adade

Overlap of [18] ec=ade with [3] cc=d:

e c cc

Critical pair: ed=adec.

Reduce RHS:

[18]	ad(ec)
	⇒ adade

Defines rule #4.

[20] ddbd=aade

Overlap of [13] dddba=ae with [12] ddbac=dbd:

d ddba ddbac

Critical pair: ddbd=aec.

Reduce RHS:

[18]	a(ec)
	⇒ aade

Defines rule #11.

Referenced by [22].

[21] dbddba=ade

Simplify [11] dbddba=ec.

Reduce RHS:

[18]	(ec)
	⇒ ade

Defines rule #17.

[22] ea=aaade

Overlap of [16] addbd=ea with [20] ddbd=aade:

a ddbd ddbd

Critical pair: aaade=ea.

Flip LHS and RHS.

Defines rule #3.