Certificate for #3814 ⟨a, b | abbababaab=a⟩

Completion settings:

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

[1] abbababaab=a

Axiom: abbababaab=a.

Referenced by [4].

[2] ababaa=c

Axiom: ababaa=c.

Referenced by [5].

[3] ab=d

Axiom: ab=d.

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

[4] dbddad=a

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

abbababaab ab

Critical pair: dbababaab=a.

Reduce LHS:

[3]	db(ab)abaab
[3]	⇒ dbd(ab)aab
[3]	⇒ dbdda(ab)
	⇒ dbddad

Referenced by [8].

[5] ddaa=c

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

ababaa ab

Critical pair: dabaa=c.

Reduce LHS:

[3]	d(ab)aa
	⇒ ddaa

Referenced by [6], [7], [12].

[6] ddad=cb

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

dda a ab

Critical pair: ddad=cb.

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

[7] cbdaa=ddac

Overlap of [6] ddad=cb with [5] ddaa=c:

dda d ddaa

Critical pair: ddac=cbdaa.

Flip LHS and RHS.

Referenced by [10].

[8] a=dbcb

Simplify [4] dbddad=a.

Reduce LHS:

[6]	db(ddad)
	⇒ dbcb

Flip LHS and RHS.

Defines rule #5.

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

[9] dbcbb=d

Overlap of [3] ab=d with [8] a=dbcb:

ab a

Critical pair: dbcbb=d.

Defines rule #3.

Referenced by [11], [14], [18], [21], [22].

[10] cbddbcbdbcb=dddbcbc

Simplify [7] cbdaa=ddac.

Reduce LHS:

[8]	cbd(a)a
[8]	⇒ cbddbcb(a)
	⇒ cbddbcbdbcb

Reduce RHS:

[8]	dd(a)c
	⇒ dddbcbc

Referenced by [11].

[11] cbddbcbd=dddbcbcb

Overlap of [10] cbddbcbdbcb=dddbcbc with [9] dbcbb=d:

cbddbcb dbcb dbcbb

Critical pair: cbddbcbd=dddbcbcb.

Referenced by [15], [21].

[12] dddbcbdbcb=c

Overlap of [5] ddaa=c with [8] a=dbcb:

dd aa a

Critical pair: dddbcba=c.

Reduce LHS:

[8]	dddbcb(a)
	⇒ dddbcbdbcb

Referenced by [17].

[13] dddbcbd=cb

Overlap of [6] ddad=cb with [8] a=dbcb:

dd ad a

Critical pair: dddbcbd=cb.

Defines rule #4.

Referenced by [14], [15], [17], [23].

[14] cbbcbb=cb

Overlap of [13] dddbcbd=cb with [9] dbcbb=d:

dddbcb d dbcbb

Critical pair: dddbcbd=cbbcbb.

Reduce LHS:

[13]	(dddbcbd)
	⇒ cb

Flip LHS and RHS.

Referenced by [16].

[15] cbdbcbd=dddbdddbcbcb

Overlap of [13] dddbcbd=cb with [11] cbddbcbd=dddbcbcb:

dddb cbd cbddbcbd

Critical pair: dddbdddbcbcb=cbdbcbd.

Flip LHS and RHS.

Referenced by [22].

[16] cbcbb=cbbcb

Overlap of [14] cbbcbb=cb with [14] cbbcbb=cb:

cbb cbb cbbcbb

Critical pair: cbbcb=cbcbb.

Flip LHS and RHS.

Referenced by [20].

[17] cbbcb=c

Simplify [12] dddbcbdbcb=c.

Reduce LHS:

[13]	(dddbcbd)bcb
	⇒ cbbcb

Defines rule #8.

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

[18] dcb=dbc

Overlap of [9] dbcbb=d with [17] cbbcb=c:

db cbb cbbcb

Critical pair: dbc=dcb.

Flip LHS and RHS.

Defines rule #1.

[19] cbcb=cbbc

Overlap of [17] cbbcb=c with [17] cbbcb=c:

cbb cb cbbcb

Critical pair: cbbc=cbcb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [21], [22].

[20] ccb=cbc

Overlap of [16] cbcbb=cbbcb with [17] cbbcb=c:

cb cbb cbbcb

Critical pair: cbc=cbbcbcb.

Reduce RHS:

[17]	(cbbcb)cb
	⇒ ccb

Flip LHS and RHS.

Defines rule #6.

[21] cbddbcbd=dddc

Simplify [11] cbddbcbd=dddbcbcb.

Reduce RHS:

[19]	dddb(cbcb)
[9]	⇒ dd(dbcbb)c
	⇒ dddc

Defines rule #10.

[22] cbdbcbd=dddbdddc

Simplify [15] cbdbcbd=dddbdddbcbcb.

Reduce RHS:

[19]	dddbdddb(cbcb)
[9]	⇒ dddbdd(dbcbb)c
	⇒ dddbdddc

Defines rule #9.

Referenced by [23].

[23] cd=dddbdddbdddc

Overlap of [13] dddbcbd=cb with [22] cbdbcbd=dddbdddc:

dddb cbd cbdbcbd

Critical pair: dddbdddbdddc=cbbcbd.

Reduce RHS:

[17]	(cbbcb)d
	⇒ cd

Flip LHS and RHS.

Defines rule #2.