Certificate for #5811 ⟨a, b | abaaab=aaaba⟩

Completion settings:

Auxiliary generators:
1. c = ab
2. d = cc
3. e = aa
4. f = ec
5. g = de
Reduction order:
- Left-to-right recursive path with deg(d) = deg(f) = deg(g) = 0, d < f < g; deg(e) = 1; deg(c) = 2; deg(a) = 3; deg(b) = 4

[1] abaaab=aaaba

Axiom: abaaab=aaaba.

Referenced by [7].

[2] ab=c

Axiom: ab=c.

Defines rule #22.

Referenced by [7], [8], [13], [14].

[3] cc=d

Axiom: cc=d.

Defines rule #11.

Referenced by [10], [11], [15].

[4] aa=e

Axiom: aa=e.

Defines rule #15.

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

[5] ec=f

Axiom: ec=f.

Defines rule #10.

Referenced by [7], [8], [9], [11], [16], [23].

[6] de=g

Axiom: de=g.

Defines rule #4.

Referenced by [9], [16], [17], [18], [19], [24].

[7] abaaab=fa

Simplify [1] abaaab=aaaba.

Reduce RHS:

[4]	(aa)aba
[2]	⇒ e(ab)a
[5]	⇒ (ec)a
	⇒ fa

Referenced by [8].

[8] fa=cf

Overlap of [7] abaaab=fa with [2] ab=c:

abaaab ab

Critical pair: caaab=fa.

Reduce LHS:

[4]	c(aa)ab
[2]	⇒ ce(ab)
[5]	⇒ c(ec)
	⇒ cf

Flip LHS and RHS.

Defines rule #12.

Referenced by [14], [15], [20].

[9] gc=df

Overlap of [6] de=g with [5] ec=f:

d e ec

Critical pair: df=gc.

Flip LHS and RHS.

Defines rule #9.

[10] dc=cd

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

c c cc

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #7.

[11] fc=ed

Overlap of [5] ec=f with [3] cc=d:

e c cc

Critical pair: ed=fc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [14], [16], [20].

[12] ea=ae

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

a a aa

Critical pair: ae=ea.

Flip LHS and RHS.

Defines rule #14.

Referenced by [18].

[13] eb=ac

Overlap of [4] aa=e with [2] ab=c:

a a ab

Critical pair: ac=eb.

Flip LHS and RHS.

Defines rule #20.

Referenced by [19], [20].

[14] cfb=ed

Overlap of [8] fa=cf with [2] ab=c:

f a ab

Critical pair: fc=cfb.

Reduce LHS:

[11]	(fc)
	⇒ ed

Flip LHS and RHS.

Defines rule #21.

Referenced by [23].

[15] fe=df

Overlap of [8] fa=cf with [4] aa=e:

f a aa

Critical pair: fe=cfa.

Reduce RHS:

[8]	c(fa)
[3]	⇒ (cc)f
	⇒ df

Defines rule #5.

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

[16] gd=ff

Overlap of [15] fe=df with [5] ec=f:

f e ec

Critical pair: ff=dfc.

Reduce RHS:

[11]	d(fc)
[6]	⇒ (de)d
	⇒ gd

Flip LHS and RHS.

Defines rule #1.

Referenced by [17], [22].

[17] fdf=gg

Overlap of [16] gd=ff with [6] de=g:

g d de

Critical pair: gg=ffe.

Reduce RHS:

[15]	f(fe)
	⇒ fdf

Flip LHS and RHS.

Defines rule #2.

Referenced by [21], [22], [24].

[18] ga=dae

Overlap of [6] de=g with [12] ea=ae:

d e ea

Critical pair: dae=ga.

Flip LHS and RHS.

Defines rule #13.

[19] gb=dac

Overlap of [6] de=g with [13] eb=ac:

d e eb

Critical pair: dac=gb.

Flip LHS and RHS.

Defines rule #16.

[20] dfb=ced

Overlap of [15] fe=df with [13] eb=ac:

f e eb

Critical pair: fac=dfb.

Reduce LHS:

[8]	(fa)c
[11]	⇒ c(fc)
	⇒ ced

Flip LHS and RHS.

Defines rule #17.

[21] gge=fddf

Overlap of [17] fdf=gg with [15] fe=df:

fd f fe

Critical pair: fddf=gge.

Flip LHS and RHS.

Defines rule #6.

[22] gfff=fdgg

Overlap of [17] fdf=gg with [17] fdf=gg:

fd f fdf

Critical pair: fdgg=ggdf.

Reduce RHS:

[16]	g(gd)f
	⇒ gfff

Flip LHS and RHS.

Defines rule #3.

[23] ffb=eed

Overlap of [5] ec=f with [14] cfb=ed:

e c cfb

Critical pair: eed=ffb.

Flip LHS and RHS.

Defines rule #18.

Referenced by [24].

[24] ggfb=fged

Overlap of [17] fdf=gg with [23] ffb=eed:

fd f ffb

Critical pair: fdeed=ggfb.

Reduce LHS:

[6]	f(de)ed
	⇒ fged

Flip LHS and RHS.

Defines rule #19.