Certificate for #3282 ⟨a, b | abbaabbabba=1⟩

Completion settings:

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

[1] abbaabbabba=1

Axiom: abbaabbabba=1.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #7.

Referenced by [3], [4], [5], [7], [9], [11], [17], [19], [32], [36], [40], [63].

[3] bbabbcbb=d

Axiom: bbabbaabb=d.

Reduce LHS:

[2]	bbabb(aa)bb
	⇒ bbabbcbb

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

[4] abbcbbabba=1

Overlap of [1] abbaabbabba=1 with [2] aa=c:

abb aabbabba aa

Critical pair: abbcbbabba=1.

Referenced by [7], [8], [9], [10], [22].

[5] ca=ac

Overlap of [2] aa=c with [2] aa=c:

a a aa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [17], [22], [27], [29], [31], [36], [38], [43], [63].

[6] bbabbcd=dabbcbb

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

bbabbc bb bbabbcbb

Critical pair: bbabbcd=dabbcbb.

Referenced by [23].

[7] cbbcbbabba=a

Overlap of [2] aa=c with [4] abbcbbabba=1:

a a abbcbbabba

Critical pair: a=cbbcbbabba.

Flip LHS and RHS.

Referenced by [25].

[8] dabba=bb

Overlap of [3] bbabbcbb=d with [4] abbcbbabba=1:

bb abbcbb abbcbbabba

Critical pair: bb=dabba.

Flip LHS and RHS.

Referenced by [11], [12], [21], [26].

[9] abbcbbabbc=a

Overlap of [4] abbcbbabba=1 with [2] aa=c:

abbcbbabb a aa

Critical pair: abbcbbabbc=a.

Referenced by [16].

[10] abbcbbad=bbcbb

Overlap of [4] abbcbbabba=1 with [3] bbabbcbb=d:

abbcbba bba bbabbcbb

Critical pair: abbcbbad=bbcbb.

Referenced by [27].

[11] bba=dabbc

Overlap of [8] dabba=bb with [2] aa=c:

dabb a aa

Critical pair: dabbc=bba.

Flip LHS and RHS.

Referenced by [13], [14], [16], [17], [20], [21], [22], [24], [25], [26], [27], [29], [30], [31], [37], [43].

[12] bbbbcbb=dad

Overlap of [8] dabba=bb with [3] bbabbcbb=d:

da bba bbabbcbb

Critical pair: dad=bbbbcbb.

Flip LHS and RHS.

Referenced by [15], [38], [39], [42].

[13] dabbcbbcbb=d

Overlap of [3] bbabbcbb=d with [11] bba=dabbc:

bbabbcbb bba

Critical pair: dabbcbbcbb=d.

Referenced by [18], [20], [25], [28].

[14] dabbcbbcdabbc=da

Overlap of [3] bbabbcbb=d with [11] bba=dabbc:

bbabbc bb bba

Critical pair: bbabbcdabbc=da.

Reduce LHS:

[11]	(bba)bbcdabbc
	⇒ dabbcbbcdabbc

Referenced by [29].

[15] bbbbcdad=dadbbcbb

Overlap of [12] bbbbcbb=dad with [12] bbbbcbb=dad:

bbbbc bb bbbbcbb

Critical pair: bbbbcdad=dadbbcbb.

Referenced by [30].

[16] abbcdabbcbbc=a

Simplify [9] abbcbbabbc=a.

Reduce LHS:

[11]	abbc(bba)bbc
	⇒ abbcdabbcbbc

Referenced by [17], [18], [20].

[17] abbcdabbcdabbcc=c

Overlap of [16] abbcdabbcbbc=a with [5] ca=ac:

abbcdabbcbb c ca

Critical pair: abbcdabbcbbac=aa.

Reduce LHS:

[11]	abbcdabbc(bba)c
	⇒ abbcdabbcdabbcc

Reduce RHS:

[2]	(aa)
	⇒ c

Referenced by [31].

[18] abbcd=abb

Overlap of [16] abbcdabbcbbc=a with [13] dabbcbbcbb=d:

abbc dabbcbbc dabbcbbcbb

Critical pair: abbcd=abb.

Referenced by [19], [20], [21], [30], [31], [34], [37].

[19] cbbcd=cbb

Overlap of [2] aa=c with [18] abbcd=abb:

a a abbcd

Critical pair: aabb=cbbcd.

Reduce LHS:

[2]	(aa)bb
	⇒ cbb

Flip LHS and RHS.

Referenced by [25], [35].

[20] adc=a

Overlap of [16] abbcdabbcbbc=a with [18] abbcd=abb:

abbcdabbcbbc abbcd

Critical pair: abbabbcbbc=a.

Reduce LHS:

[11]	a(bba)bbcbbc
[13]	⇒ a(dabbcbbcbb)c
	⇒ adc

Referenced by [32], [38], [43], [47], [48].

[21] abbcbb=abbbbc

Overlap of [18] abbcd=abb with [8] dabba=bb:

abbc d dabba

Critical pair: abbcbb=abbabba.

Reduce RHS:

[11]	a(bba)bba
[11]	⇒ adabbc(bba)
[18]	⇒ ad(abbcd)abbc
[8]	⇒ a(dabba)bbc
	⇒ abbbbc

Referenced by [22], [23], [24], [27], [28], [29], [31].

[22] abbdabbccdabbc=1

Overlap of [4] abbcbbabba=1 with [21] abbcbb=abbbbc:

abbcbbabba abbcbb

Critical pair: abbbbcabba=1.

Reduce LHS:

[5]	abbbb(ca)bba
[11]	⇒ abb(bba)cbba
[11]	⇒ abbdabbcc(bba)
	⇒ abbdabbccdabbc

Referenced by [43].

[23] bbabbcd=dabbbbc

Simplify [6] bbabbcd=dabbcbb.

Reduce RHS:

[21]	d(abbcbb)
	⇒ dabbbbc

Referenced by [24].

[24] dabbbbccd=dabbbbc

Overlap of [23] bbabbcd=dabbbbc with [11] bba=dabbc:

bbabbcd bba

Critical pair: dabbcbbcd=dabbbbc.

Reduce LHS:

[21]	d(abbcbb)cd
	⇒ dabbbbccd

Referenced by [29], [31].

[25] cda=a

Overlap of [7] cbbcbbabba=a with [11] bba=dabbc:

cbbc bbabba bba

Critical pair: cbbcdabbcbba=a.

Reduce LHS:

[19]	(cbbcd)abbcbba
[11]	⇒ c(bba)bbcbba
[13]	⇒ c(dabbcbbcbb)a
	⇒ cda

Referenced by [30], [33], [36], [38].

[26] dadabbc=bb

Overlap of [8] dabba=bb with [11] bba=dabbc:

da bba bba

Critical pair: dadabbc=bb.

Referenced by [33], [34], [35].

[27] abbdabbccd=bbcbb

Overlap of [10] abbcbbad=bbcbb with [21] abbcbb=abbbbc:

abbcbbad abbcbb

Critical pair: abbbbcad=bbcbb.

Reduce LHS:

[5]	abbbb(ca)d
[11]	⇒ abb(bba)cd
	⇒ abbdabbccd

Referenced by [43], [44].

[28] dabbbbccbb=d

Overlap of [13] dabbcbbcbb=d with [21] abbcbb=abbbbc:

d abbcbbcbb abbcbb

Critical pair: dabbbbccbb=d.

Referenced by [46].

[29] dabbdabbccbbc=da

Overlap of [14] dabbcbbcdabbc=da with [21] abbcbb=abbbbc:

d abbcbbcdabbc abbcbb

Critical pair: dabbbbccdabbc=da.

Reduce LHS:

[24]	(dabbbbccd)abbc
[5]	⇒ dabbbb(ca)bbc
[11]	⇒ dabb(bba)cbbc
	⇒ dabbdabbccbbc

Referenced by [31], [47].

[30] bbdabb=dadbbcbb

Overlap of [15] bbbbcdad=dadbbcbb with [25] cda=a:

bbbb cdad cda

Critical pair: bbbbad=dadbbcbb.

Reduce LHS:

[11]	bb(bba)d
[18]	⇒ bbd(abbcd)
	⇒ bbdabb

Referenced by [43], [45], [47].

[31] adac=c

Overlap of [17] abbcdabbcdabbcc=c with [18] abbcd=abb:

abbcdabbcdabbcc abbcd

Critical pair: abbabbcdabbcc=c.

Reduce LHS:

[11]	a(bba)bbcdabbcc
[21]	⇒ ad(abbcbb)cdabbcc
[24]	⇒ a(dabbbbccd)abbcc
[5]	⇒ adabbbb(ca)bbcc
[11]	⇒ adabb(bba)cbbcc
[29]	⇒ a(dabbdabbccbbc)c
	⇒ adac

Referenced by [41].

[32] cdc=c

Overlap of [2] aa=c with [20] adc=a:

a a adc

Critical pair: aa=cdc.

Reduce LHS:

[2]	(aa)
	⇒ c

Flip LHS and RHS.

Referenced by [37].

[33] adabbc=cbb

Overlap of [25] cda=a with [26] dadabbc=bb:

c da dadabbc

Critical pair: cbb=adabbc.

Flip LHS and RHS.

Referenced by [36], [37].

[34] dadabb=bbd

Overlap of [26] dadabbc=bb with [18] abbcd=abb:

dad abbc abbcd

Critical pair: dadabb=bbd.

Referenced by [35], [37].

[35] bbdcbb=bbbbcd

Overlap of [26] dadabbc=bb with [19] cbbcd=cbb:

dadabb c cbbcd

Critical pair: dadabbcbb=bbbbcd.

Reduce LHS:

[34]	(dadabb)cbb
	⇒ bbdcbb

Referenced by [37].

[36] ccbb=cbbc

Overlap of [5] ca=ac with [33] adabbc=cbb:

c a adabbc

Critical pair: ccbb=acdabbc.

Reduce RHS:

[25]	a(cda)bbc
[2]	⇒ (aa)bbc
	⇒ cbbc

Referenced by [38], [39], [43], [46], [47], [53].

[37] bbcbb=bbbbc

Overlap of [11] bba=dabbc with [33] adabbc=cbb:

bb a adabbc

Critical pair: bbcbb=dabbcdabbc.

Reduce RHS:

[18]	d(abbcd)abbc
[11]	⇒ da(bba)bbc
[34]	⇒ (dadabb)cbbc
[35]	⇒ (bbdcbb)c
[32]	⇒ bbbb(cdc)
	⇒ bbbbc

Referenced by [38], [39], [42], [43], [44], [45], [46], [47].

[38] acd=a

Overlap of [36] ccbb=cbbc with [12] bbbbcbb=dad:

cc bb bbbbcbb

Critical pair: ccdad=cbbcbbcbb.

Reduce LHS:

[25]	c(cda)d
[5]	⇒ (ca)d
	⇒ acd

Reduce RHS:

[37]	c(bbcbb)cbb
[36]	⇒ cbbbb(ccbb)
[12]	⇒ c(bbbbcbb)c
[25]	⇒ (cda)dc
[20]	⇒ (adc)
	⇒ a

Referenced by [40], [41], [51].

[39] cbbbbcbcbb=ccbdad

Overlap of [36] ccbb=cbbc with [12] bbbbcbb=dad:

ccb b bbbbcbb

Critical pair: ccbdad=cbbcbbbcbb.

Reduce RHS:

[37]	c(bbcbb)bcbb
	⇒ cbbbbcbcbb

Flip LHS and RHS.

Referenced by [56].

[40] ccd=c

Overlap of [2] aa=c with [38] acd=a:

a a acd

Critical pair: aa=ccd.

Reduce LHS:

[2]	(aa)
	⇒ c

Flip LHS and RHS.

Referenced by [45], [54].

[41] ada=cd

Overlap of [31] adac=c with [38] acd=a:

ad ac acd

Critical pair: ada=cd.

Referenced by [45], [46], [47], [48], [52].

[42] bbbbbbc=dad

Overlap of [12] bbbbcbb=dad with [37] bbcbb=bbbbc:

bb bbcbb bbcbb

Critical pair: bbbbbbc=dad.

Referenced by [43], [46], [47], [57], [58].

[43] daddacc=1

Overlap of [22] abbdabbccdabbc=1 with [27] abbdabbccd=bbcbb:

abbdabbccdabbc abbdabbccd

Critical pair: bbcbbabbc=1.

Reduce LHS:

[37]	(bbcbb)abbc
[5]	⇒ bbbb(ca)bbc
[11]	⇒ bb(bba)cbbc
[30]	⇒ (bbdabb)ccbbc
[37]	⇒ dad(bbcbb)ccbbc
[36]	⇒ dadbbbbc(ccbb)c
[36]	⇒ dadbbbb(ccbb)cc
[37]	⇒ dadbb(bbcbb)ccc
[42]	⇒ dad(bbbbbbc)ccc
[20]	⇒ dadd(adc)cc
	⇒ daddacc

Referenced by [52].

[44] abbdabbccd=bbbbc

Simplify [27] abbdabbccd=bbcbb.

Reduce RHS:

[37]	(bbcbb)
	⇒ bbbbc

Referenced by [45].

[45] cddbbbbcc=bbbbc

Overlap of [44] abbdabbccd=bbbbc with [30] bbdabb=dadbbcbb:

a bbdabbccd bbdabb

Critical pair: adadbbcbbccd=bbbbc.

Reduce LHS:

[41]	(ada)dbbcbbccd
[37]	⇒ cdd(bbcbb)ccd
[40]	⇒ cddbbbbc(ccd)
	⇒ cddbbbbcc

Referenced by [47].

[46] dcddc=d

Overlap of [28] dabbbbccbb=d with [36] ccbb=cbbc:

dabbbb ccbb ccbb

Critical pair: dabbbbcbbc=d.

Reduce LHS:

[37]	dabb(bbcbb)c
[42]	⇒ da(bbbbbbc)c
[41]	⇒ d(ada)dc
	⇒ dcddc

Referenced by [49].

[47] ddac=da

Overlap of [29] dabbdabbccbbc=da with [30] bbdabb=dadbbcbb:

da bbdabbccbbc bbdabb

Critical pair: dadadbbcbbccbbc=da.

Reduce LHS:

[41]	d(ada)dbbcbbccbbc
[37]	⇒ dcdd(bbcbb)ccbbc
[45]	⇒ d(cddbbbbcc)cbbc
[36]	⇒ dbbbb(ccbb)c
[37]	⇒ dbb(bbcbb)cc
[42]	⇒ d(bbbbbbc)cc
[20]	⇒ dd(adc)c
	⇒ ddac

Referenced by [51].

[48] cddc=cd

Overlap of [41] ada=cd with [20] adc=a:

ad a adc

Critical pair: ada=cddc.

Reduce LHS:

[41]	(ada)
	⇒ cd

Flip LHS and RHS.

Referenced by [49], [50].

[49] dcd=d

Simplify [46] dcddc=d.

Reduce LHS:

[48]	d(cddc)
	⇒ dcd

Referenced by [50], [52].

[50] ddc=d

Overlap of [49] dcd=d with [48] cddc=cd:

d cd cddc

Critical pair: dcd=ddc.

Reduce LHS:

[49]	(dcd)
	⇒ d

Flip LHS and RHS.

Referenced by [52], [57].

[51] dda=dad

Overlap of [47] ddac=da with [38] acd=a:

dd ac acd

Critical pair: dda=dad.

Referenced by [52], [55].

[52] dc=1

Simplify [43] daddacc=1.

Reduce LHS:

[51]	da(dda)cc
[41]	⇒ d(ada)dcc
[49]	⇒ (dcd)dcc
[50]	⇒ (ddc)c
	⇒ dc

Defines rule #1.

Referenced by [53], [54], [59], [60], [61], [62], [75].

[53] cbb=bbc

Overlap of [52] dc=1 with [36] ccbb=cbbc:

d c ccbb

Critical pair: dcbbc=cbb.

Reduce LHS:

[52]	(dc)bbc
	⇒ bbc

Flip LHS and RHS.

Defines rule #9.

Referenced by [57].

[54] cd=1

Overlap of [52] dc=1 with [40] ccd=c:

d c ccd

Critical pair: dc=cd.

Reduce LHS:

[52]	(dc)
	⇒ 1

Flip LHS and RHS.

Defines rule #2.

Referenced by [55], [63], [64], [65], [66], [67], [68], [69], [70], [71], [72], [73], [74], [76].

[55] da=ad

Overlap of [54] cd=1 with [51] dda=dad:

c d dda

Critical pair: cdad=da.

Reduce LHS:

[54]	(cd)ad
	⇒ ad

Flip LHS and RHS.

Defines rule #4.

Referenced by [56], [57], [58], [59], [60], [63].

[56] cbbbbcbcbb=ccbadd

Simplify [39] cbbbbcbcbb=ccbdad.

Reduce RHS:

[55]	ccb(da)d
	⇒ ccbadd

Referenced by [57].

[57] ccbadd=adbc

Overlap of [56] cbbbbcbcbb=ccbadd with [53] cbb=bbc:

cbbbbcbcbb cbb

Critical pair: bbcbbcbcbb=ccbadd.

Reduce LHS:

[53]	bb(cbb)cbcbb
[53]	⇒ bbbbccb(cbb)
[53]	⇒ bbbbc(cbb)bc
[53]	⇒ bbbb(cbb)cbc
[42]	⇒ (bbbbbbc)cbc
[55]	⇒ (da)dcbc
[50]	⇒ a(ddc)bc
	⇒ adbc

Flip LHS and RHS.

Referenced by [59].

[58] bbbbbbc=add

Simplify [42] bbbbbbc=dad.

Reduce RHS:

[55]	(da)d
	⇒ add

Referenced by [64].

[59] cbadd=addbc

Overlap of [52] dc=1 with [57] ccbadd=adbc:

d c ccbadd

Critical pair: dadbc=cbadd.

Reduce LHS:

[55]	(da)dbc
	⇒ addbc

Flip LHS and RHS.

Referenced by [60].

[60] badd=adddbc

Overlap of [52] dc=1 with [59] cbadd=addbc:

d c cbadd

Critical pair: daddbc=badd.

Reduce LHS:

[55]	(da)ddbc
	⇒ adddbc

Flip LHS and RHS.

Referenced by [61].

[61] bad=adddbcc

Overlap of [60] badd=adddbc with [52] dc=1:

bad d dc

Critical pair: bad=adddbcc.

Referenced by [62].

[62] ba=adddbccc

Overlap of [61] bad=adddbcc with [52] dc=1:

ba d dc

Critical pair: ba=adddbccc.

Referenced by [63], [75].

[63] dddddbcccccc=bc

Overlap of [62] ba=adddbccc with [2] aa=c:

b a aa

Critical pair: bc=adddbccca.

Reduce RHS:

[5]	adddbcc(ca)
[5]	⇒ adddbc(ca)c
[5]	⇒ adddb(ca)cc
[62]	⇒ addd(ba)ccc
[55]	⇒ add(da)dddbcccccc
[55]	⇒ ad(da)ddddbcccccc
[55]	⇒ a(da)dddddbcccccc
[2]	⇒ (aa)ddddddbcccccc
[54]	⇒ (cd)dddddbcccccc
	⇒ dddddbcccccc