Certificate for #2991 ⟨a, b | aaabbbabbba=1⟩

Completion settings:

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

[1] aaabbbabbba=1

Axiom: aaabbbabbba=1.

Referenced by [4].

[2] bbb=c

Axiom: bbb=c.

Defines rule #8.

Referenced by [4], [6].

[3] acac=d

Axiom: acac=d.

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

[4] aada=1

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

aaa bbbabbba bbb

Critical pair: aaacabbba=1.

Reduce LHS:

[2]	aaaca(bbb)a
[3]	⇒ aa(acac)a
	⇒ aada

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

[5] aad=ada

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

aad a aada

Critical pair: aad=ada.

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

[6] cb=bc

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

b bb bbb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [16].

[7] acd=dac

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

ac ac acac

Critical pair: acd=dac.

Referenced by [12].

[8] cac=adad

Overlap of [4] aada=1 with [3] acac=d:

aad a acac

Critical pair: aadd=cac.

Reduce LHS:

[5]	(aad)d
	⇒ adad

Flip LHS and RHS.

Referenced by [15].

[9] adaa=1

Overlap of [4] aada=1 with [5] aad=ada:

aada aad

Critical pair: adaa=1.

Referenced by [10], [11].

[10] ad=da

Overlap of [4] aada=1 with [5] aad=ada:

aad a aad

Critical pair: aadada=ad.

Reduce LHS:

[5]	(aad)ada
[9]	⇒ (adaa)da
	⇒ da

Flip LHS and RHS.

Defines rule #1.

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

[11] daaa=1

Simplify [9] adaa=1.

Reduce LHS:

[10]	(ad)aa
	⇒ daaa

Defines rule #2.

Referenced by [12], [13], [18], [19], [20].

[12] cd=dc

Overlap of [4] aada=1 with [7] acd=dac:

aad a acd

Critical pair: aaddac=cd.

Reduce LHS:

[5]	(aad)dac
[10]	⇒ (ad)adac
[5]	⇒ d(aad)ac
[10]	⇒ d(ad)aac
[11]	⇒ d(daaa)c
	⇒ dc

Flip LHS and RHS.

Defines rule #3.

Referenced by [13].

[13] dcaaa=c

Overlap of [12] cd=dc with [11] daaa=1:

c d daaa

Critical pair: c=dcaaa.

Flip LHS and RHS.

Referenced by [14].

[14] daacaaa=aac

Overlap of [5] aad=ada with [13] dcaaa=c:

aa d dcaaa

Critical pair: aac=adacaaa.

Reduce RHS:

[10]	(ad)acaaa
	⇒ daacaaa

Flip LHS and RHS.

Referenced by [18].

[15] cac=ddaa

Simplify [8] cac=adad.

Reduce RHS:

[10]	(ad)ad
[10]	⇒ da(ad)
[10]	⇒ d(ad)a
	⇒ ddaa

Defines rule #5.

Referenced by [16], [17].

[16] cabc=ddaab

Overlap of [15] cac=ddaa with [6] cb=bc:

ca c cb

Critical pair: cabc=ddaab.

Referenced by [17].

[17] cabddaa=ddaabac

Overlap of [16] cabc=ddaab with [15] cac=ddaa:

cab c cac

Critical pair: cabddaa=ddaabac.

Referenced by [19].

[18] caaa=aaac

Overlap of [10] ad=da with [14] daacaaa=aac:

a d daacaaa

Critical pair: aaac=daaacaaa.

Reduce RHS:

[11]	(daaa)caaa
	⇒ caaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [20].

[19] cabd=ddaabaca

Overlap of [17] cabddaa=ddaabac with [11] daaa=1:

cabd daa daaa

Critical pair: cabd=ddaabaca.

Referenced by [20].

[20] cab=ddaabaaaaca

Overlap of [19] cabd=ddaabaca with [11] daaa=1:

cab d daaa

Critical pair: cab=ddaabacaaaa.

Reduce RHS:

[18]	ddaaba(caaa)a
	⇒ ddaabaaaaca

Defines rule #7.