Certificate for #678 ⟨a, b | aabbaaabb=1⟩

Completion settings:

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

[1] aabbaaabb=1

Axiom: aabbaaabb=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #9.

Referenced by [4], [5], [6], [10], [14], [22], [30].

[3] bbaabb=d

Axiom: bbaabb=d.

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

[4] aabbcbb=1

Overlap of [1] aabbaaabb=1 with [2] aaa=c:

aabb aaabb aaa

Critical pair: aabbcbb=1.

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

[5] ca=ac

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

a aa aaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #4.

Referenced by [18], [29].

[6] cbbcbb=a

Overlap of [2] aaa=c with [4] aabbcbb=1:

a aa aabbcbb

Critical pair: a=cbbcbb.

Flip LHS and RHS.

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

[7] dcbb=bb

Overlap of [3] bbaabb=d with [4] aabbcbb=1:

bb aabb aabbcbb

Critical pair: bb=dcbb.

Flip LHS and RHS.

Referenced by [9], [10].

[8] baabb=aabbcbd

Overlap of [4] aabbcbb=1 with [3] bbaabb=d:

aabbcb b bbaabb

Critical pair: aabbcbd=baabb.

Flip LHS and RHS.

Referenced by [29].

[9] bbcbb=da

Overlap of [7] dcbb=bb with [6] cbbcbb=a:

d cbb cbbcbb

Critical pair: da=bbcbb.

Flip LHS and RHS.

Referenced by [10], [11], [13], [20].

[10] bbcd=bb

Overlap of [9] bbcbb=da with [3] bbaabb=d:

bbc bb bbaabb

Critical pair: bbcd=daaabb.

Reduce RHS:

[2]	d(aaa)bb
[7]	⇒ (dcbb)
	⇒ bb

Referenced by [12].

[11] bba=dacbb

Overlap of [9] bbcbb=da with [6] cbbcbb=a:

bb cbb cbbcbb

Critical pair: bba=dacbb.

Referenced by [21].

[12] acd=a

Overlap of [6] cbbcbb=a with [10] bbcd=bb:

cbbc bb bbcd

Critical pair: cbbcbb=acd.

Reduce LHS:

[6]	(cbbcbb)
	⇒ a

Flip LHS and RHS.

Referenced by [15], [19].

[13] aada=1

Overlap of [4] aabbcbb=1 with [9] bbcbb=da:

aa bbcbb bbcbb

Critical pair: aada=1.

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

[14] aadc=aa

Overlap of [13] aada=1 with [2] aaa=c:

aad a aaa

Critical pair: aadc=aa.

Referenced by [16].

[15] cd=1

Overlap of [13] aada=1 with [12] acd=a:

aad a acd

Critical pair: aada=cd.

Reduce LHS:

[13]	(aada)
	⇒ 1

Flip LHS and RHS.

Defines rule #1.

Referenced by [25], [30], [31], [32], [33], [34], [35].

[16] adc=a

Overlap of [13] aada=1 with [14] aadc=aa:

aad a aadc

Critical pair: aadaa=adc.

Reduce LHS:

[13]	(aada)a
	⇒ a

Flip LHS and RHS.

Referenced by [17], [21].

[17] dc=1

Overlap of [13] aada=1 with [16] adc=a:

aad a adc

Critical pair: aada=dc.

Reduce LHS:

[13]	(aada)
	⇒ 1

Flip LHS and RHS.

Defines rule #2.

Referenced by [18], [23], [27], [28], [30], [36].

[18] dac=a

Overlap of [17] dc=1 with [5] ca=ac:

d c ca

Critical pair: dac=a.

Referenced by [19].

[19] da=ad

Overlap of [18] dac=a with [12] acd=a:

d ac acd

Critical pair: da=ad.

Defines rule #3.

Referenced by [20], [21], [24], [29].

[20] bbcbb=ad

Simplify [9] bbcbb=da.

Reduce RHS:

[19]	(da)
	⇒ ad

Referenced by [24].

[21] bba=abb

Simplify [11] bba=dacbb.

Reduce RHS:

[19]	(da)cbb
[16]	⇒ (adc)bb
	⇒ abb

Referenced by [22], [30].

[22] cbb=bbc

Overlap of [21] bba=abb with [2] aaa=c:

bb a aaa

Critical pair: bbc=abbaa.

Reduce RHS:

[21]	a(bba)a
[21]	⇒ aa(bba)
[2]	⇒ (aaa)bb
	⇒ cbb

Flip LHS and RHS.

Referenced by [23], [29].

[23] dbbc=bb

Overlap of [17] dc=1 with [22] cbb=bbc:

d c cbb

Critical pair: dbbc=bb.

Referenced by [24], [25].

[24] bbbb=add

Overlap of [23] dbbc=bb with [20] bbcbb=ad:

d bbc bbcbb

Critical pair: dad=bbbb.

Reduce LHS:

[19]	(da)d
	⇒ add

Flip LHS and RHS.

Defines rule #10.

Referenced by [26], [30].

[25] dbb=bbd

Overlap of [23] dbbc=bb with [15] cd=1:

dbb c cd

Critical pair: dbb=bbd.

Defines rule #8.

Referenced by [29].

[26] badd=addb

Overlap of [24] bbbb=add with [24] bbbb=add:

b bbb bbbb

Critical pair: badd=addb.

Referenced by [27].

[27] bad=addbc

Overlap of [26] badd=addb with [17] dc=1:

bad d dc

Critical pair: bad=addbc.

Referenced by [28].

[28] ba=addbcc

Overlap of [27] bad=addbc with [17] dc=1:

ba d dc

Critical pair: ba=addbcc.

Defines rule #7.

Referenced by [29].

[29] aabbcbd=aabbddddbcccc

Simplify [8] baabb=aabbcbd.

Reduce LHS:

[28]	(ba)abb
[5]	⇒ addbc(ca)bb
[5]	⇒ addb(ca)cbb
[28]	⇒ add(ba)ccbb
[19]	⇒ ad(da)ddbccccbb
[19]	⇒ a(da)dddbccccbb
[22]	⇒ aaddddbccc(cbb)
[22]	⇒ aaddddbcc(cbb)c
[22]	⇒ aaddddbc(cbb)cc
[22]	⇒ aaddddb(cbb)ccc
[25]	⇒ aaddd(dbb)bcccc
[25]	⇒ aadd(dbb)dbcccc
[25]	⇒ aad(dbb)ddbcccc
[25]	⇒ aa(dbb)dddbcccc
	⇒ aabbddddbcccc