Certificate for #1379 ⟨a, b | aaabbbaaba=1⟩

Completion settings:

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

[1] aaabbbaaba=1

Axiom: aaabbbaaba=1.

Referenced by [4].

[2] bbb=c

Axiom: bbb=c.

Defines rule #5.

Referenced by [4], [5], [14], [24], [29], [32].

[3] aabaaaa=d

Axiom: aabaaaa=d.

Defines rule #17.

Referenced by [6], [7], [8], [9], [16], [17], [21].

[4] aaacaaba=1

Overlap of [1] aaabbbaaba=1 with [2] bbb=c:

aaa bbbaaba bbb

Critical pair: aaacaaba=1.

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

[5] cb=bc

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

b bb bbb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [19], [30].

[6] aabaad=dbaaaa

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

aabaa aa aabaaaa

Critical pair: aabaad=dbaaaa.

Referenced by [26].

[7] aabaaad=dabaaaa

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

aabaaa a aabaaaa

Critical pair: aabaaad=dabaaaa.

Defines rule #14.

Referenced by [34].

[8] dcaaba=aaba

Overlap of [3] aabaaaa=d with [4] aaacaaba=1:

aaba aaa aaacaaba

Critical pair: aaba=dcaaba.

Flip LHS and RHS.

Referenced by [11].

[9] dacaaba=aabaa

Overlap of [3] aabaaaa=d with [4] aaacaaba=1:

aabaa aa aaacaaba

Critical pair: aabaa=dacaaba.

Flip LHS and RHS.

Referenced by [21], [25].

[10] aaacaab=aacaaba

Overlap of [4] aaacaaba=1 with [4] aaacaaba=1:

aaacaab a aaacaaba

Critical pair: aaacaab=aacaaba.

Referenced by [11], [12].

[11] aabaacaabaa=dcaab

Overlap of [8] dcaaba=aaba with [4] aaacaaba=1:

dcaab a aaacaaba

Critical pair: dcaab=aabaaacaaba.

Reduce RHS:

[10]	aab(aaacaab)a
	⇒ aabaacaabaa

Flip LHS and RHS.

Referenced by [13].

[12] aacaabaa=1

Overlap of [4] aaacaaba=1 with [10] aaacaab=aacaaba:

aaacaaba aaacaab

Critical pair: aacaabaa=1.

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

[13] dcaab=aab

Overlap of [11] aabaacaabaa=dcaab with [12] aacaabaa=1:

aab aacaabaa aacaabaa

Critical pair: aab=dcaab.

Flip LHS and RHS.

Referenced by [14].

[14] dcaac=aac

Overlap of [13] dcaab=aab with [2] bbb=c:

dcaa b bbb

Critical pair: dcaac=aabbb.

Reduce RHS:

[2]	aa(bbb)
	⇒ aac

Referenced by [16].

[15] aacaab=caabaa

Overlap of [12] aacaabaa=1 with [12] aacaabaa=1:

aacaab aa aacaabaa

Critical pair: aacaab=caabaa.

Referenced by [16], [17].

[16] cd=dc

Overlap of [14] dcaac=aac with [12] aacaabaa=1:

dc aac aacaabaa

Critical pair: dc=aacaabaa.

Reduce RHS:

[15]	(aacaab)aa
[3]	⇒ c(aabaaaa)
	⇒ cd

Flip LHS and RHS.

Referenced by [17], [18].

[17] dc=1

Overlap of [12] aacaabaa=1 with [15] aacaab=caabaa:

aacaabaa aacaab

Critical pair: caabaaaa=1.

Reduce LHS:

[3]	c(aabaaaa)
[16]	⇒ (cd)
	⇒ dc

Defines rule #1.

Referenced by [18], [19], [22], [27], [35].

[18] cd=1

Simplify [16] cd=dc.

Reduce RHS:

[17]	(dc)
	⇒ 1

Defines rule #2.

Referenced by [20], [23], [25], [29], [31], [32], [33].

[19] dbc=b

Overlap of [17] dc=1 with [5] cb=bc:

d c cb

Critical pair: dbc=b.

Referenced by [20].

[20] db=bd

Overlap of [19] dbc=b with [18] cd=1:

db c cd

Critical pair: db=bd.

Defines rule #4.

Referenced by [26], [28], [31], [34].

[21] dacaabd=aabad

Overlap of [9] dacaaba=aabaa with [3] aabaaaa=d:

dacaab a aabaaaa

Critical pair: dacaabd=aabaaabaaaa.

Reduce RHS:

[3]	aaba(aabaaaa)
	⇒ aabad

Referenced by [22].

[22] dacaab=aaba

Overlap of [21] dacaabd=aabad with [17] dc=1:

dacaab d dc

Critical pair: dacaab=aabadc.

Reduce RHS:

[17]	aaba(dc)
	⇒ aaba

Referenced by [23], [24].

[23] acaab=caaba

Overlap of [18] cd=1 with [22] dacaab=aaba:

c d dacaab

Critical pair: caaba=acaab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [33].

[24] aababb=dacaac

Overlap of [22] dacaab=aaba with [2] bbb=c:

dacaa b bbb

Critical pair: dacaac=aababb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [25].

[25] aabaabb=daacaac

Overlap of [9] dacaaba=aabaa with [24] aababb=dacaac:

dac aaba aababb

Critical pair: dacdacaac=aabaabb.

Reduce LHS:

[18]	da(cd)acaac
	⇒ daacaac

Flip LHS and RHS.

Defines rule #13.

Referenced by [31], [33].

[26] aabaad=bdaaaa

Simplify [6] aabaad=dbaaaa.

Reduce RHS:

[20]	(db)aaaa
	⇒ bdaaaa

Defines rule #9.

Referenced by [27], [28].

[27] bdaaaac=aabaa

Overlap of [26] aabaad=bdaaaa with [17] dc=1:

aabaa d dc

Critical pair: aabaa=bdaaaac.

Flip LHS and RHS.

Referenced by [29].

[28] aabaabd=bdaaaab

Overlap of [26] aabaad=bdaaaa with [20] db=bd:

aabaa d db

Critical pair: aabaabd=bdaaaab.

Defines rule #11.

Referenced by [31].

[29] aaaac=bbaabaa

Overlap of [2] bbb=c with [27] bdaaaac=aabaa:

bb b bdaaaac

Critical pair: bbaabaa=cdaaaac.

Reduce RHS:

[18]	(cd)aaaac
	⇒ aaaac

Flip LHS and RHS.

Defines rule #8.

Referenced by [30].

[30] aaaabc=bbaabaab

Overlap of [29] aaaac=bbaabaa with [5] cb=bc:

aaaa c cb

Critical pair: aaaabc=bbaabaab.

Defines rule #10.

[31] bdaaaabb=daacaa

Overlap of [28] aabaabd=bdaaaab with [20] db=bd:

aabaab d db

Critical pair: aabaabbd=bdaaaabb.

Reduce LHS:

[25]	(aabaabb)d
[18]	⇒ daacaa(cd)
	⇒ daacaa

Flip LHS and RHS.

Referenced by [32].

[32] aaaabb=bbdaacaa

Overlap of [2] bbb=c with [31] bdaaaabb=daacaa:

bb b bdaaaabb

Critical pair: bbdaacaa=cdaaaabb.

Reduce RHS:

[18]	(cd)aaaabb
	⇒ aaaabb

Flip LHS and RHS.

Defines rule #12.

[33] caabaaabb=aaacaac

Overlap of [23] acaab=caaba with [25] aabaabb=daacaac:

ac aab aabaabb

Critical pair: acdaacaac=caabaaabb.

Reduce LHS:

[18]	a(cd)aacaac
	⇒ aaacaac

Flip LHS and RHS.

Referenced by [35].

[34] aabaaabd=dabaaaab

Overlap of [7] aabaaad=dabaaaa with [20] db=bd:

aabaaa d db

Critical pair: aabaaabd=dabaaaab.

Defines rule #15.

[35] aabaaabb=daaacaac

Overlap of [17] dc=1 with [33] caabaaabb=aaacaac:

d c caabaaabb

Critical pair: daaacaac=aabaaabb.

Flip LHS and RHS.

Defines rule #16.