Certificate for #2228 ⟨a, b, c | aabc=1, cbac=1⟩

Completion settings:

Auxiliary generators:
1. d = ccb
2. e = caa
3. f = cba
Reduction order:
- Left-to-right shortlex with c < f < a < b < e < d

[1] aabc=1

Axiom: aabc=1.

Referenced by [13].

[2] cbac=1

Axiom: cbac=1.

Referenced by [6].

[3] ccb=d

Axiom: ccb=d.

Defines rule #15.

Referenced by [7], [10], [25], [37].

[4] caa=e

Axiom: caa=e.

Referenced by [8].

[5] cba=f

Axiom: cba=f.

Referenced by [6], [10], [11], [14].

[6] fc=1

Overlap of [2] cbac=1 with [5] cba=f:

cbac cba

Critical pair: fc=1.

Defines rule #2.

Referenced by [7], [8], [11], [19], [21], [24].

[7] fd=cb

Overlap of [6] fc=1 with [3] ccb=d:

f c ccb

Critical pair: fd=cb.

Defines rule #3.

Referenced by [22], [34], [39].

[8] aa=fe

Overlap of [6] fc=1 with [4] caa=e:

f c caa

Critical pair: fe=aa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [9], [12], [13], [26].

[9] afe=fea

Overlap of [8] aa=fe with [8] aa=fe:

a a aa

Critical pair: afe=fea.

Defines rule #19.

Referenced by [20].

[10] da=cf

Overlap of [3] ccb=d with [5] cba=f:

c cb cba

Critical pair: cf=da.

Flip LHS and RHS.

Referenced by [23], [27].

[11] ba=ff

Overlap of [6] fc=1 with [5] cba=f:

f c cba

Critical pair: ff=ba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [12], [14], [18], [24], [41], [43].

[12] bfe=ffa

Overlap of [11] ba=ff with [8] aa=fe:

b a aa

Critical pair: bfe=ffa.

Defines rule #22.

Referenced by [42].

[13] febc=1

Simplify [1] aabc=1.

Reduce LHS:

[8]	(aa)bc
	⇒ febc

Referenced by [15], [16].

[14] cff=f

Overlap of [5] cba=f with [11] ba=ff:

c ba ba

Critical pair: cff=f.

Referenced by [15].

[15] cf=1

Overlap of [14] cff=f with [13] febc=1:

cf f febc

Critical pair: cf=febc.

Reduce RHS:

[13]	(febc)
	⇒ 1

Defines rule #1.

Referenced by [16], [17], [23], [27], [28], [38].

[16] feb=f

Overlap of [13] febc=1 with [15] cf=1:

feb c cf

Critical pair: feb=f.

Referenced by [17].

[17] eb=1

Overlap of [15] cf=1 with [16] feb=f:

c f feb

Critical pair: cf=eb.

Reduce LHS:

[15]	(cf)
	⇒ 1

Flip LHS and RHS.

Defines rule #9.

Referenced by [18], [25].

[18] eff=a

Overlap of [17] eb=1 with [11] ba=ff:

e b ba

Critical pair: eff=a.

Referenced by [19].

[19] ef=ac

Overlap of [18] eff=a with [6] fc=1:

ef f fc

Critical pair: ef=ac.

Defines rule #8.

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

[20] afac=feaf

Overlap of [9] afe=fea with [19] ef=ac:

af e ef

Critical pair: afac=feaf.

Defines rule #31.

[21] acc=e

Overlap of [19] ef=ac with [6] fc=1:

e f fc

Critical pair: e=acc.

Flip LHS and RHS.

Defines rule #18.

Referenced by [23], [24], [25], [32].

[22] ecb=acd

Overlap of [19] ef=ac with [7] fd=cb:

e f fd

Critical pair: ecb=acd.

Defines rule #24.

[23] de=cc

Overlap of [10] da=cf with [21] acc=e:

d a acc

Critical pair: de=cfcc.

Reduce RHS:

[15]	(cf)cc
	⇒ cc

Defines rule #13.

Referenced by [29], [31].

[24] be=1

Overlap of [11] ba=ff with [21] acc=e:

b a acc

Critical pair: be=ffcc.

Reduce RHS:

[6]	f(fc)c
[6]	⇒ (fc)
	⇒ 1

Defines rule #7.

Referenced by [30].

[25] ad=1

Overlap of [21] acc=e with [3] ccb=d:

a cc ccb

Critical pair: ad=eb.

Reduce RHS:

[17]	(eb)
	⇒ 1

Defines rule #5.

Referenced by [26], [33], [35].

[26] fed=a

Overlap of [8] aa=fe with [25] ad=1:

a a ad

Critical pair: a=fed.

Flip LHS and RHS.

Referenced by [28].

[27] da=1

Simplify [10] da=cf.

Reduce RHS:

[15]	(cf)
	⇒ 1

Defines rule #12.

[28] ed=ca

Overlap of [15] cf=1 with [26] fed=a:

c f fed

Critical pair: ca=ed.

Flip LHS and RHS.

Defines rule #10.

Referenced by [29], [30], [31], [40].

[29] dca=ccd

Overlap of [23] de=cc with [28] ed=ca:

d e ed

Critical pair: dca=ccd.

Defines rule #27.

[30] bca=d

Overlap of [24] be=1 with [28] ed=ca:

b e ed

Critical pair: bca=d.

Defines rule #21.

Referenced by [32], [33].

[31] ecc=cae

Overlap of [28] ed=ca with [23] de=cc:

e d de

Critical pair: ecc=cae.

Defines rule #23.

[32] dcc=bce

Overlap of [30] bca=d with [21] acc=e:

bc a acc

Critical pair: bce=dcc.

Flip LHS and RHS.

Defines rule #26.

[33] dd=bc

Overlap of [30] bca=d with [25] ad=1:

bc a ad

Critical pair: bc=dd.

Flip LHS and RHS.

Defines rule #14.

Referenced by [34], [35], [36].

[34] fbc=cbd

Overlap of [7] fd=cb with [33] dd=bc:

f d dd

Critical pair: fbc=cbd.

Defines rule #17.

[35] abc=d

Overlap of [25] ad=1 with [33] dd=bc:

a d dd

Critical pair: abc=d.

Defines rule #20.

Referenced by [37], [38].

[36] dbc=bcd

Overlap of [33] dd=bc with [33] dd=bc:

d d dd

Critical pair: dbc=bcd.

Defines rule #29.

[37] dcb=abd

Overlap of [35] abc=d with [3] ccb=d:

ab c ccb

Critical pair: abd=dcb.

Flip LHS and RHS.

Defines rule #28.

[38] df=ab

Overlap of [35] abc=d with [15] cf=1:

ab c cf

Critical pair: ab=df.

Flip LHS and RHS.

Defines rule #11.

Referenced by [39], [40].

[39] fab=cbf

Overlap of [7] fd=cb with [38] df=ab:

f d df

Critical pair: fab=cbf.

Defines rule #16.

Referenced by [41].

[40] eab=caf

Overlap of [28] ed=ca with [38] df=ab:

e d df

Critical pair: eab=caf.

Defines rule #25.

Referenced by [43].

[41] faff=cbfa

Overlap of [39] fab=cbf with [11] ba=ff:

fa b ba

Critical pair: faff=cbfa.

Defines rule #30.

[42] bfac=ffaf

Overlap of [12] bfe=ffa with [19] ef=ac:

bf e ef

Critical pair: bfac=ffaf.

Defines rule #32.

[43] eaff=cafa

Overlap of [40] eab=caf with [11] ba=ff:

ea b ba

Critical pair: eaff=cafa.

Defines rule #33.