Certificate for #2461 ⟨a, b | aaabba=baaa⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(a) = deg(f) = 0, a < f; deg(e) = 1; deg(d) = deg(c) = deg(b) = 2, d < c < b
Auxiliary generators:
1. bba=c
2. cc=d
3. dad=e
4. eaa=f

[1] aaabba=baaa

Axiom: aaabba=baaa.

Referenced by [6].

[2] bba=c

Axiom: bba=c.

Defines rule #21.

Referenced by [6], [12].

[3] cc=d

Axiom: cc=d.

Defines rule #20.

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

[4] dad=e

Axiom: dad=e.

Defines rule #17.

Referenced by [8], [9], [11], [13], [15].

[5] eaa=f

Axiom: eaa=f.

Defines rule #4.

Referenced by [10], [14], [15], [16], [17], [24].

[6] baaa=aaac

Overlap of [1] aaabba=baaa with [2] bba=c:

aaa bba bba

Critical pair: aaac=baaa.

Flip LHS and RHS.

Defines rule #15.

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

[7] dc=cd

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

c c cc

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #18.

Referenced by [9].

[8] dae=ead

Overlap of [4] dad=e with [4] dad=e:

da d dad

Critical pair: dae=ead.

Defines rule #9.

Referenced by [10].

[9] dacd=ec

Overlap of [4] dad=e with [7] dc=cd:

da d dc

Critical pair: dacd=ec.

Defines rule #22.

Referenced by [11].

[10] daf=eadaa

Overlap of [8] dae=ead with [5] eaa=f:

da e eaa

Critical pair: daf=eadaa.

Referenced by [14].

[11] dace=ecad

Overlap of [9] dacd=ec with [4] dad=e:

dac d dad

Critical pair: dace=ecad.

Defines rule #19.

[12] caa=aaad

Overlap of [2] bba=c with [6] baaa=aaac:

b ba baaa

Critical pair: baaac=caa.

Reduce LHS:

[6]	(baaa)c
[3]	⇒ aaa(cc)
	⇒ aaad

Flip LHS and RHS.

Defines rule #11.

Referenced by [13], [20], [21], [22].

[13] daa=aaae

Overlap of [3] cc=d with [12] caa=aaad:

c c caa

Critical pair: caaad=daa.

Reduce LHS:

[12]	(caa)ad
[4]	⇒ aaa(dad)
	⇒ aaae

Flip LHS and RHS.

Defines rule #7.

Referenced by [14], [15], [22], [23].

[14] daf=faae

Simplify [10] daf=eadaa.

Reduce RHS:

[13]	ea(daa)
[5]	⇒ (eaa)aae
	⇒ faae

Defines rule #8.

Referenced by [21].

[15] aaafe=f

Overlap of [4] dad=e with [13] daa=aaae:

da d daa

Critical pair: daaaae=eaa.

Reduce LHS:

[13]	(daa)aae
[5]	⇒ aaa(eaa)e
	⇒ aaafe

Reduce RHS:

[5]	(eaa)
	⇒ f

Defines rule #2.

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

[16] ef=fafe

Overlap of [5] eaa=f with [15] aaafe=f:

e aa aaafe

Critical pair: ef=fafe.

Defines rule #3.

Referenced by [22].

[17] eaf=faafe

Overlap of [5] eaa=f with [15] aaafe=f:

ea a aaafe

Critical pair: eaf=faafe.

Defines rule #5.

Referenced by [23].

[18] bf=aaacfe

Overlap of [6] baaa=aaac with [15] aaafe=f:

b aaa aaafe

Critical pair: bf=aaacfe.

Referenced by [25].

[19] baf=aaacafe

Overlap of [6] baaa=aaac with [15] aaafe=f:

ba aa aaafe

Critical pair: baf=aaacafe.

Referenced by [26].

[20] baaf=aaaaaadfe

Overlap of [6] baaa=aaac with [15] aaafe=f:

baa a aaafe

Critical pair: baaf=aaacaafe.

Reduce RHS:

[12]	aaa(caa)fe
	⇒ aaaaaadfe

Referenced by [27].

[21] cf=aaafaaee

Overlap of [12] caa=aaad with [15] aaafe=f:

c aa aaafe

Critical pair: cf=aaadafe.

Reduce RHS:

[14]	aaa(daf)e
	⇒ aaafaaee

Defines rule #10.

Referenced by [25].

[22] caf=aaaaaafafee

Overlap of [12] caa=aaad with [15] aaafe=f:

ca a aaafe

Critical pair: caf=aaadaafe.

Reduce RHS:

[13]	aaa(daa)fe
[16]	⇒ aaaaaa(ef)e
	⇒ aaaaaafafee

Defines rule #12.

Referenced by [26].

[23] df=aaafaafee

Overlap of [13] daa=aaae with [15] aaafe=f:

d aa aaafe

Critical pair: df=aaaeafe.

Reduce RHS:

[17]	aaa(eaf)e
	⇒ aaafaafee

Defines rule #6.

Referenced by [27].

[24] aaaff=faa

Overlap of [15] aaafe=f with [5] eaa=f:

aaaf e eaa

Critical pair: aaaff=faa.

Defines rule #1.

[25] bf=aaaaaafaaeee

Simplify [18] bf=aaacfe.

Reduce RHS:

[21]	aaa(cf)e
	⇒ aaaaaafaaeee

Defines rule #13.

[26] baf=aaaaaaaaafafeee

Simplify [19] baf=aaacafe.

Reduce RHS:

[22]	aaa(caf)e
	⇒ aaaaaaaaafafeee

Defines rule #14.

[27] baaf=aaaaaaaaafaafeee

Simplify [20] baaf=aaaaaadfe.

Reduce RHS:

[23]	aaaaaa(df)e
	⇒ aaaaaaaaafaafeee

Defines rule #16.