Certificate for #2783 ⟨a, b | aaaaaaaabba=1⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b < c < d
Auxiliary generators:
1. aaaaaaaaa=c
2. bb=d

[1] aaaaaaaabba=1

Axiom: aaaaaaaabba=1.

Referenced by [4].

[2] aaaaaaaaa=c

Axiom: aaaaaaaaa=c.

Defines rule #8.

Referenced by [6], [7], [14], [16].

[3] bb=d

Axiom: bb=d.

Defines rule #1.

Referenced by [4], [5].

[4] aaaaaaaada=1

Overlap of [1] aaaaaaaabba=1 with [3] bb=d:

aaaaaaaa bba bb

Critical pair: aaaaaaaada=1.

Referenced by [7], [8], [9], [11], [12], [13].

[5] db=bd

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

b b bb

Critical pair: bd=db.

Flip LHS and RHS.

Defines rule #6.

Referenced by [10].

[6] ca=ac

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

a aaaaaaaa aaaaaaaaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #2.

Referenced by [18].

[7] cda=a

Overlap of [2] aaaaaaaaa=c with [4] aaaaaaaada=1:

a aaaaaaaa aaaaaaaada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9].

[8] aaaaaaada=aaaaaaaad

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

aaaaaaaad a aaaaaaaada

Critical pair: aaaaaaaad=aaaaaaada.

Flip LHS and RHS.

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

[9] cd=1

Overlap of [7] cda=a with [4] aaaaaaaada=1:

cd a aaaaaaaada

Critical pair: cd=aaaaaaaada.

Reduce RHS:

[4]	(aaaaaaaada)
	⇒ 1

Defines rule #4.

Referenced by [10], [14], [16], [19].

[10] cbd=b

Overlap of [9] cd=1 with [5] db=bd:

c d db

Critical pair: cbd=b.

Referenced by [17].

[11] aaaaaada=aaaaaaad

Overlap of [4] aaaaaaaada=1 with [8] aaaaaaada=aaaaaaaad:

aaaaaaaad a aaaaaaada

Critical pair: aaaaaaaadaaaaaaaad=aaaaaada.

Reduce LHS:

[4]	(aaaaaaaada)aaaaaaad
	⇒ aaaaaaad

Flip LHS and RHS.

Referenced by [13].

[12] aaaaada=aaaaaad

Overlap of [8] aaaaaaada=aaaaaaaad with [8] aaaaaaada=aaaaaaaad:

aaaaaaad a aaaaaaada

Critical pair: aaaaaaadaaaaaaaad=aaaaaaaadaaaaaada.

Reduce LHS:

[8]	(aaaaaaada)aaaaaaad
[4]	⇒ (aaaaaaaada)aaaaaad
	⇒ aaaaaad

Reduce RHS:

[4]	(aaaaaaaada)aaaaada
	⇒ aaaaada

Flip LHS and RHS.

Referenced by [13].

[13] ada=aad

Overlap of [12] aaaaada=aaaaaad with [12] aaaaada=aaaaaad:

aaaaad a aaaaada

Critical pair: aaaaadaaaaaad=aaaaaadaaaada.

Reduce LHS:

[12]	(aaaaada)aaaaad
[11]	⇒ (aaaaaada)aaaad
[8]	⇒ (aaaaaaada)aaad
[4]	⇒ (aaaaaaaada)aad
	⇒ aad

Reduce RHS:

[11]	(aaaaaada)aaada
[8]	⇒ (aaaaaaada)aada
[4]	⇒ (aaaaaaaada)ada
	⇒ ada

Flip LHS and RHS.

Referenced by [14], [15].

[14] adc=a

Overlap of [13] ada=aad with [2] aaaaaaaaa=c:

ad a aaaaaaaaa

Critical pair: adc=aadaaaaaaaa.

Reduce RHS:

[13]	a(ada)aaaaaaa
[13]	⇒ aa(ada)aaaaaa
[13]	⇒ aaa(ada)aaaaa
[13]	⇒ aaaa(ada)aaaa
[13]	⇒ aaaaa(ada)aaa
[13]	⇒ aaaaaa(ada)aa
[13]	⇒ aaaaaaa(ada)a
[2]	⇒ (aaaaaaaaa)da
[9]	⇒ (cd)a
	⇒ a

Referenced by [15].

[15] aaddc=aad

Overlap of [13] ada=aad with [14] adc=a:

ad a adc

Critical pair: ada=aaddc.

Reduce LHS:

[13]	(ada)
	⇒ aad

Flip LHS and RHS.

Referenced by [16].

[16] dc=1

Overlap of [2] aaaaaaaaa=c with [15] aaddc=aad:

aaaaaaa aa aaddc

Critical pair: aaaaaaaaad=cddc.

Reduce LHS:

[2]	(aaaaaaaaa)d
[9]	⇒ (cd)
	⇒ 1

Reduce RHS:

[9]	(cd)dc
	⇒ dc

Flip LHS and RHS.

Defines rule #7.

Referenced by [17], [18].

[17] cb=bc

Overlap of [10] cbd=b with [16] dc=1:

cb d dc

Critical pair: cb=bc.

Defines rule #3.

[18] dac=a

Overlap of [16] dc=1 with [6] ca=ac:

d c ca

Critical pair: dac=a.

Referenced by [19].

[19] da=ad

Overlap of [18] dac=a with [9] cd=1:

da c cd

Critical pair: da=ad.

Defines rule #5.