Certificate for #4485 ⟨a, b | aaabaaab=aba⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(c) = deg(e) = 0, c < e; deg(d) = 1; deg(a) = deg(b) = 2, a < b
Auxiliary generators:
1. ab=c
2. aa=d
3. cdd=e

[1] aaabaaab=aba

Axiom: aaabaaab=aba.

Referenced by [5].

[2] ab=c

Axiom: ab=c.

Defines rule #30.

Referenced by [5], [6], [8], [11].

[3] aa=d

Axiom: aa=d.

Defines rule #29.

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

[4] cdd=e

Axiom: cdd=e.

Defines rule #5.

Referenced by [9], [10], [12], [13], [14], [15], [18], [19], [21], [22], [23].

[5] aaabaaab=ca

Simplify [1] aaabaaab=aba.

Reduce RHS:

[2]	(ab)a
	⇒ ca

Referenced by [6].

[6] ca=dcdc

Overlap of [5] aaabaaab=ca with [3] aa=d:

aaabaaab aa

Critical pair: dabaaab=ca.

Reduce LHS:

[2]	d(ab)aaab
[3]	⇒ dc(aa)ab
[2]	⇒ dcd(ab)
	⇒ dcdc

Flip LHS and RHS.

Defines rule #19.

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

[7] da=ad

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

a a aa

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #21.

Referenced by [9], [10].

[8] db=ac

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

a a ab

Critical pair: ac=db.

Flip LHS and RHS.

Defines rule #24.

Referenced by [10].

[9] ea=dcde

Overlap of [4] cdd=e with [7] da=ad:

cd d da

Critical pair: cdad=ea.

Reduce LHS:

[7]	c(da)d
[6]	⇒ (ca)dd
[4]	⇒ dcd(cdd)
	⇒ dcde

Flip LHS and RHS.

Defines rule #20.

Referenced by [13].

[10] eb=dcdcdc

Overlap of [4] cdd=e with [8] db=ac:

cd d db

Critical pair: cdac=eb.

Reduce LHS:

[7]	c(da)c
[6]	⇒ (ca)dc
	⇒ dcdcdc

Flip LHS and RHS.

Referenced by [20].

[11] dcdcb=cc

Overlap of [6] ca=dcdc with [2] ab=c:

c a ab

Critical pair: cc=dcdcb.

Flip LHS and RHS.

Defines rule #28.

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

[12] decdc=cd

Overlap of [6] ca=dcdc with [3] aa=d:

c a aa

Critical pair: cd=dcdca.

Reduce RHS:

[6]	dcd(ca)
[4]	⇒ d(cdd)cdc
	⇒ decdc

Flip LHS and RHS.

Defines rule #2.

Referenced by [14], [16], [19], [22], [25], [32].

[13] decde=ed

Overlap of [9] ea=dcde with [3] aa=d:

e a aa

Critical pair: ed=dcdea.

Reduce RHS:

[9]	dcd(ea)
[4]	⇒ d(cdd)cde
	⇒ decde

Flip LHS and RHS.

Defines rule #3.

Referenced by [15], [16], [17], [21], [26], [28], [30], [33].

[14] cdcd=eecdc

Overlap of [4] cdd=e with [12] decdc=cd:

cd d decdc

Critical pair: cdcd=eecdc.

Defines rule #6.

Referenced by [20], [22], [23], [24], [25], [26], [27], [29], [31].

[15] cded=eecde

Overlap of [4] cdd=e with [13] decde=ed:

cd d decde

Critical pair: cded=eecde.

Defines rule #7.

Referenced by [30], [31], [32], [33].

[16] edcdc=deccd

Overlap of [13] decde=ed with [12] decdc=cd:

dec de decdc

Critical pair: deccd=edcdc.

Flip LHS and RHS.

Defines rule #9.

[17] edcde=deced

Overlap of [13] decde=ed with [13] decde=ed:

dec de decde

Critical pair: deced=edcde.

Flip LHS and RHS.

Defines rule #10.

[18] ecdcb=cdcc

Overlap of [4] cdd=e with [11] dcdcb=cc:

cd d dcdcb

Critical pair: cdcc=ecdcb.

Flip LHS and RHS.

Defines rule #26.

[19] ecb=deccc

Overlap of [12] decdc=cd with [11] dcdcb=cc:

dec dc dcdcb

Critical pair: deccc=cddcb.

Reduce RHS:

[4]	(cdd)cb
	⇒ ecb

Flip LHS and RHS.

Defines rule #23.

Referenced by [21].

[20] eb=deecdcc

Simplify [10] eb=dcdcdc.

Reduce RHS:

[14]	d(cdcd)c
	⇒ deecdcc

Defines rule #22.

[21] edcb=deeeccc

Overlap of [13] decde=ed with [19] ecb=deccc:

decd e ecb

Critical pair: decddeccc=edcb.

Reduce LHS:

[4]	de(cdd)eccc
	⇒ deeeccc

Flip LHS and RHS.

Defines rule #25.

[22] deeecdc=e

Overlap of [12] decdc=cd with [14] cdcd=eecdc:

de cdc cdcd

Critical pair: deeecdc=cdd.

Reduce RHS:

[4]	(cdd)
	⇒ e

Defines rule #4.

Referenced by [28], [29].

[23] eeeecdc=cde

Overlap of [14] cdcd=eecdc with [4] cdd=e:

cd cd cdd

Critical pair: cde=eecdcd.

Reduce RHS:

[14]	ee(cdcd)
	⇒ eeeecdc

Flip LHS and RHS.

Defines rule #1.

[24] eecdccb=ccc

Overlap of [14] cdcd=eecdc with [11] dcdcb=cc:

c dcd dcdcb

Critical pair: ccc=eecdccb.

Flip LHS and RHS.

Defines rule #27.

[25] eecdcecdc=cdccd

Overlap of [14] cdcd=eecdc with [12] decdc=cd:

cdc d decdc

Critical pair: cdccd=eecdcecdc.

Flip LHS and RHS.

Defines rule #14.

[26] eecdcecde=cdced

Overlap of [14] cdcd=eecdc with [13] decde=ed:

cdc d decde

Critical pair: cdced=eecdcecde.

Flip LHS and RHS.

Defines rule #15.

[27] eecdccd=cdeecdc

Overlap of [14] cdcd=eecdc with [14] cdcd=eecdc:

cd cd cdcd

Critical pair: cdeecdc=eecdccd.

Flip LHS and RHS.

Defines rule #12.

[28] edeecdc=dece

Overlap of [13] decde=ed with [22] deeecdc=e:

dec de deeecdc

Critical pair: dece=edeecdc.

Flip LHS and RHS.

Defines rule #11.

[29] eecdceeecdc=cdce

Overlap of [14] cdcd=eecdc with [22] deeecdc=e:

cdc d deeecdc

Critical pair: cdce=eecdceeecdc.

Flip LHS and RHS.

Defines rule #18.

[30] edd=deeecde

Overlap of [13] decde=ed with [15] cded=eecde:

de cde cded

Critical pair: deeecde=edd.

Flip LHS and RHS.

Defines rule #8.

[31] eecdced=cdeecde

Overlap of [14] cdcd=eecdc with [15] cded=eecde:

cd cd cded

Critical pair: cdeecde=eecdced.

Flip LHS and RHS.

Defines rule #13.

[32] eecdeecdc=cdecd

Overlap of [15] cded=eecde with [12] decdc=cd:

cde d decdc

Critical pair: cdecd=eecdeecdc.

Flip LHS and RHS.

Defines rule #16.

[33] eecdeecde=cdeed

Overlap of [15] cded=eecde with [13] decde=ed:

cde d decde

Critical pair: cdeed=eecdeecde.

Flip LHS and RHS.

Defines rule #17.