Certificate for #1465 ⟨a, b | aabbbabbba=1⟩

Completion settings:

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

[1] aabbbabbba=1

Axiom: aabbbabbba=1.

Referenced by [4].

[2] abbb=c

Axiom: abbb=c.

Referenced by [4], [6], [9].

[3] aa=d

Axiom: aa=d.

Defines rule #5.

Referenced by [4], [5], [6], [8], [10], [17], [20].

[4] dbbbca=1

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

aabbbabbba aa

Critical pair: dbbbabbba=1.

Reduce LHS:

[2]	dbbb(abbb)a
	⇒ dbbbca

Referenced by [7].

[5] da=ad

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

a a aa

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #3.

Referenced by [13], [21].

[6] dbbb=ac

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

a a abbb

Critical pair: ac=dbbb.

Flip LHS and RHS.

Referenced by [7].

[7] acca=1

Simplify [4] dbbbca=1.

Reduce LHS:

[6]	(dbbb)ca
	⇒ acca

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

[8] dcca=a

Overlap of [3] aa=d with [7] acca=1:

a a acca

Critical pair: a=dcca.

Flip LHS and RHS.

Referenced by [13].

[9] bbb=accc

Overlap of [7] acca=1 with [2] abbb=c:

acc a abbb

Critical pair: accc=bbb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [16].

[10] accd=a

Overlap of [7] acca=1 with [3] aa=d:

acc a aa

Critical pair: accd=a.

Referenced by [12].

[11] cca=acc

Overlap of [7] acca=1 with [7] acca=1:

acc a acca

Critical pair: acc=cca.

Flip LHS and RHS.

Defines rule #4.

Referenced by [13], [17].

[12] ccd=1

Overlap of [7] acca=1 with [10] accd=a:

acc a accd

Critical pair: acca=ccd.

Reduce LHS:

[7]	(acca)
	⇒ 1

Flip LHS and RHS.

Defines rule #2.

Referenced by [15], [17], [18], [19], [20], [22].

[13] adcc=a

Simplify [8] dcca=a.

Reduce LHS:

[11]	d(cca)
[5]	⇒ (da)cc
	⇒ adcc

Referenced by [14].

[14] dcc=1

Overlap of [7] acca=1 with [13] adcc=a:

acc a adcc

Critical pair: acca=dcc.

Reduce LHS:

[7]	(acca)
	⇒ 1

Flip LHS and RHS.

Referenced by [15].

[15] dc=cd

Overlap of [14] dcc=1 with [12] ccd=1:

dc c ccd

Critical pair: dc=cd.

Defines rule #1.

Referenced by [17], [19], [20], [21].

[16] baccc=acccb

Overlap of [9] bbb=accc with [9] bbb=accc:

b bb bbb

Critical pair: baccc=acccb.

Referenced by [17], [18].

[17] acccbca=bcc

Overlap of [16] baccc=acccb with [11] cca=acc:

bacc c cca

Critical pair: baccacc=acccbca.

Reduce LHS:

[11]	ba(cca)cc
[3]	⇒ b(aa)cccc
[15]	⇒ b(dc)ccc
[15]	⇒ bc(dc)cc
[12]	⇒ b(ccd)cc
	⇒ bcc

Flip LHS and RHS.

Referenced by [20].

[18] bac=acccbd

Overlap of [16] baccc=acccb with [12] ccd=1:

bac cc ccd

Critical pair: bac=acccbd.

Referenced by [19].

[19] ba=acccbcdd

Overlap of [18] bac=acccbd with [12] ccd=1:

ba c ccd

Critical pair: ba=acccbdcd.

Reduce RHS:

[15]	acccb(dc)d
	⇒ acccbcdd

Defines rule #6.

[20] cbca=abcc

Overlap of [3] aa=d with [17] acccbca=bcc:

a a acccbca

Critical pair: abcc=dcccbca.

Reduce RHS:

[15]	(dc)ccbca
[15]	⇒ c(dc)cbca
[12]	⇒ (ccd)cbca
	⇒ cbca

Flip LHS and RHS.

Referenced by [21].

[21] cdbca=adbcc

Overlap of [15] dc=cd with [20] cbca=abcc:

d c cbca

Critical pair: dabcc=cdbca.

Reduce LHS:

[5]	(da)bcc
	⇒ adbcc

Flip LHS and RHS.

Referenced by [22].

[22] bca=cadbcc

Overlap of [12] ccd=1 with [21] cdbca=adbcc:

c cd cdbca

Critical pair: cadbcc=bca.

Flip LHS and RHS.

Defines rule #7.