Certificate for #1709 ⟨a, b | aabbaaaab=a⟩

Completion settings:

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

[1] aabbaaaab=a

Axiom: aabbaaaab=a.

Referenced by [3].

[2] aaaa=c

Axiom: aaaa=c.

Referenced by [3], [4], [5], [6], [8].

[3] aabbcb=a

Overlap of [1] aabbaaaab=a with [2] aaaa=c:

aabb aaaab aaaa

Critical pair: aabbcb=a.

Referenced by [5], [6], [7], [10], [14].

[4] ca=ac

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

a aaa aaaa

Critical pair: ac=ca.

Flip LHS and RHS.

Referenced by [6], [7], [9], [15].

[5] aaa=cbbcb

Overlap of [2] aaaa=c with [3] aabbcb=a:

aa aa aabbcb

Critical pair: aaa=cbbcb.

Referenced by [6], [8], [9], [10], [11], [16].

[6] cbbcba=acbbcb

Overlap of [2] aaaa=c with [3] aabbcb=a:

aaa a aabbcb

Critical pair: aaaa=cabbcb.

Reduce LHS:

[5]	(aaa)a
	⇒ cbbcba

Reduce RHS:

[4]	(ca)bbcb
	⇒ acbbcb

Referenced by [8], [16].

[7] aacbbcb=ac

Overlap of [4] ca=ac with [3] aabbcb=a:

c a aabbcb

Critical pair: ca=acabbcb.

Reduce LHS:

[4]	(ca)
	⇒ ac

Reduce RHS:

[4]	a(ca)bbcb
	⇒ aacbbcb

Flip LHS and RHS.

Referenced by [12].

[8] acbbcb=c

Overlap of [2] aaaa=c with [5] aaa=cbbcb:

aaaa aaa

Critical pair: cbbcba=c.

Reduce LHS:

[6]	(cbbcba)
	⇒ acbbcb

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

[9] ccbbcb=cbbcbc

Overlap of [4] ca=ac with [5] aaa=cbbcb:

c a aaa

Critical pair: ccbbcb=acaa.

Reduce RHS:

[4]	a(ca)a
[4]	⇒ aa(ca)
[5]	⇒ (aaa)c
	⇒ cbbcbc

Defines rule #1.

Referenced by [15].

[10] aa=cbbcbbbcb

Overlap of [5] aaa=cbbcb with [3] aabbcb=a:

a aa aabbcb

Critical pair: aa=cbbcbbbcb.

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

[11] cbbcbcbbcb=cbbcbbbcbc

Overlap of [5] aaa=cbbcb with [8] acbbcb=c:

aa a acbbcb

Critical pair: aac=cbbcbcbbcb.

Reduce LHS:

[10]	(aa)c
	⇒ cbbcbbbcbc

Flip LHS and RHS.

Defines rule #4.

Referenced by [15], [19].

[12] ac=cbbcbbbcbcbbcb

Simplify [7] aacbbcb=ac.

Reduce LHS:

[10]	(aa)cbbcb
	⇒ cbbcbbbcbcbbcb

Flip LHS and RHS.

Referenced by [13], [17].

[13] cbbcbbbcbcbbcbbbcb=c

Overlap of [8] acbbcb=c with [12] ac=cbbcbbbcbcbbcb:

acbbcb ac

Critical pair: cbbcbbbcbcbbcbbbcb=c.

Referenced by [16].

[14] a=cbbcbbbcbbbcb

Overlap of [3] aabbcb=a with [10] aa=cbbcbbbcb:

aabbcb aa

Critical pair: cbbcbbbcbbbcb=a.

Flip LHS and RHS.

Defines rule #11.

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

[15] cbbcbbbcbbbcbcbbcbbbcbbbcbc=cbbcbbbcbc

Overlap of [4] ca=ac with [10] aa=cbbcbbbcb:

c a aa

Critical pair: ccbbcbbbcb=aca.

Reduce LHS:

[9]	(ccbbcb)bbcb
[11]	⇒ (cbbcbcbbcb)
	⇒ cbbcbbbcbc

Reduce RHS:

[14]	(a)ca
[4]	⇒ cbbcbbbcbbbcb(ca)
[14]	⇒ cbbcbbbcbbbcb(a)c
	⇒ cbbcbbbcbbbcbcbbcbbbcbbbcbc

Flip LHS and RHS.

Referenced by [16].

[16] cbbcbbbcbbbcbcbbcb=c

Overlap of [5] aaa=cbbcb with [10] aa=cbbcbbbcb:

aa a aa

Critical pair: aacbbcbbbcb=cbbcba.

Reduce LHS:

[14]	(a)acbbcbbbcb
[14]	⇒ cbbcbbbcbbbcb(a)cbbcbbbcb
[15]	⇒ (cbbcbbbcbbbcbcbbcbbbcbbbcbc)bbcbbbcb
[13]	⇒ (cbbcbbbcbcbbcbbbcb)
	⇒ c

Reduce RHS:

[6]	(cbbcba)
[14]	⇒ (a)cbbcb
	⇒ cbbcbbbcbbbcbcbbcb

Flip LHS and RHS.

Defines rule #10.

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

[17] cbbcbbbcbcbbcb=cbbcbbbcbbbcbc

Overlap of [12] ac=cbbcbbbcbcbbcb with [14] a=cbbcbbbcbbbcb:

ac a

Critical pair: cbbcbbbcbbbcbc=cbbcbbbcbcbbcb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [21].

[18] cbcbbbcbbbcbcbbcb=cbbcbbbcbbbcbcbbc

Overlap of [8] acbbcb=c with [16] cbbcbbbcbbbcbcbbcb=c:

acbb cb cbbcbbbcbbbcbcbbcb

Critical pair: acbbc=cbcbbbcbbbcbcbbcb.

Reduce LHS:

[14]	(a)cbbc
	⇒ cbbcbbbcbbbcbcbbc

Flip LHS and RHS.

Defines rule #9.

Referenced by [23].

[19] cbcbcbbcb=cbcbbbcbc

Overlap of [16] cbbcbbbcbbbcbcbbcb=c with [11] cbbcbcbbcb=cbbcbbbcbc:

cbbcbbbcbbbcbcbb cb cbbcbcbbcb

Critical pair: cbbcbbbcbbbcbcbbcbbcbbbcbc=cbcbcbbcb.

Reduce LHS:

[16]	(cbbcbbbcbbbcbcbbcb)bcbbbcbc
	⇒ cbcbbbcbc

Flip LHS and RHS.

Defines rule #3.

Referenced by [20].

[20] ccbcbbcb=ccbbbcbc

Overlap of [16] cbbcbbbcbbbcbcbbcb=c with [19] cbcbcbbcb=cbcbbbcbc:

cbbcbbbcbbbcbcbb cb cbcbcbbcb

Critical pair: cbbcbbbcbbbcbcbbcbcbbbcbc=ccbcbbcb.

Reduce LHS:

[16]	(cbbcbbbcbbbcbcbbcb)cbbbcbc
	⇒ ccbbbcbc

Flip LHS and RHS.

Defines rule #2.

[21] cbcbbbcbcbbcb=cbcbbbcbbbcbc

Overlap of [16] cbbcbbbcbbbcbcbbcb=c with [17] cbbcbbbcbcbbcb=cbbcbbbcbbbcbc:

cbbcbbbcbbbcbcbb cb cbbcbbbcbcbbcb

Critical pair: cbbcbbbcbbbcbcbbcbbcbbbcbbbcbc=cbcbbbcbcbbcb.

Reduce LHS:

[16]	(cbbcbbbcbbbcbcbbcb)bcbbbcbbbcbc
	⇒ cbcbbbcbbbcbc

Flip LHS and RHS.

Defines rule #6.

Referenced by [22].

[22] ccbbbcbcbbcb=ccbbbcbbbcbc

Overlap of [16] cbbcbbbcbbbcbcbbcb=c with [21] cbcbbbcbcbbcb=cbcbbbcbbbcbc:

cbbcbbbcbbbcbcbb cb cbcbbbcbcbbcb

Critical pair: cbbcbbbcbbbcbcbbcbcbbbcbbbcbc=ccbbbcbcbbcb.

Reduce LHS:

[16]	(cbbcbbbcbbbcbcbbcb)cbbbcbbbcbc
	⇒ ccbbbcbbbcbc

Flip LHS and RHS.

Defines rule #5.

[23] ccbbbcbbbcbcbbcb=cbcbbbcbbbcbcbbc

Overlap of [16] cbbcbbbcbbbcbcbbcb=c with [18] cbcbbbcbbbcbcbbcb=cbbcbbbcbbbcbcbbc:

cbbcbbbcbbbcbcbb cb cbcbbbcbbbcbcbbcb

Critical pair: cbbcbbbcbbbcbcbbcbbcbbbcbbbcbcbbc=ccbbbcbbbcbcbbcb.

Reduce LHS:

[16]	(cbbcbbbcbbbcbcbbcb)bcbbbcbbbcbcbbc
	⇒ cbcbbbcbbbcbcbbc

Flip LHS and RHS.

Defines rule #8.