Certificate for #1 ⟨a, b, c, d | dcbadab=aa, ac=1, ca=1, bd=1, db=1⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(e) = deg(f) = deg(a) = deg(c) = 0, e < f < a < c; deg(g) = 1; deg(b) = 2; deg(d) = 3
• Auxiliary generators:
  1. dcb=e
  2. ce=f
  3. dab=g

Axiom: dcbadab=aa.

Referenced by [9].

Axiom: ac=1.

Defines rule #3.

Referenced by [10], [18], [27], [29], [30].

Axiom: ca=1.

Defines rule #6.

Referenced by [13], [24], [25], [28].

Axiom: bd=1.

Defines rule #20.

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

Axiom: db=1.

Defines rule #14.

Referenced by [16], [19].

Axiom: dcb=e.

Referenced by [9], [14], [15], [16].

Axiom: ce=f.

Defines rule #4.

Referenced by [10], [17], [24].

Axiom: dab=g.

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

Overlap of [1] dcbadab=aa with [6] dcb=e:

Critical pair: eadab=aa.

Reduce LHS:

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

Overlap of [2] ac=1 with [7] ce=f:

Critical pair: e=af.

Flip LHS and RHS.

Defines rule #2.

Overlap of [4] bd=1 with [8] dab=g:

Critical pair: ab=bg.

Defines rule #12.

Referenced by [13], [18].

Overlap of [8] dab=g with [4] bd=1:

Critical pair: gd=da.

Defines rule #19.

Referenced by [20], [21].

Overlap of [3] ca=1 with [11] ab=bg:

Critical pair: b=cbg.

Flip LHS and RHS.

Referenced by [16].

Overlap of [4] bd=1 with [6] dcb=e:

Critical pair: cb=be.

Defines rule #13.

Referenced by [18].

Overlap of [6] dcb=e with [4] bd=1:

Critical pair: ed=dc.

Defines rule #15.

Referenced by [26].

Overlap of [6] dcb=e with [13] cbg=b:

Critical pair: eg=db.

Reduce RHS:

Defines rule #8.

Referenced by [17].

Overlap of [7] ce=f with [16] eg=1:

Critical pair: fg=c.

Defines rule #9.

Referenced by [20].

Overlap of [2] ac=1 with [14] cb=be:

Critical pair: b=abe.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [5] db=1 with [18] bge=b:

Critical pair: ge=db.

Reduce RHS:

Defines rule #7.

Referenced by [22], [23].

Overlap of [17] fg=c with [12] gd=da:

Critical pair: cd=fda.

Defines rule #16.

Overlap of [9] eag=aa with [12] gd=da:

Critical pair: aad=eada.

Defines rule #18.

Overlap of [9] eag=aa with [19] ge=1:

Critical pair: aae=ea.

Referenced by [24].

Overlap of [19] ge=1 with [9] eag=aa:

Critical pair: ag=gaa.

Defines rule #10.

Referenced by [28].

Overlap of [3] ca=1 with [22] aae=ea:

Critical pair: ae=cea.

Reduce RHS:

Defines rule #1.

Referenced by [25], [26].

Overlap of [3] ca=1 with [24] ae=fa:

Critical pair: e=cfa.

Flip LHS and RHS.

Referenced by [27].

Overlap of [24] ae=fa with [15] ed=dc:

Critical pair: fad=adc.

Defines rule #17.

Overlap of [25] cfa=e with [2] ac=1:

Critical pair: ec=cf.

Flip LHS and RHS.

Defines rule #5.

Overlap of [3] ca=1 with [23] ag=gaa:

Critical pair: g=cgaa.

Flip LHS and RHS.

Referenced by [29].

Overlap of [28] cgaa=g with [2] ac=1:

Critical pair: gc=cga.

Flip LHS and RHS.

Referenced by [30].

Overlap of [29] cga=gc with [2] ac=1:

Critical pair: gcc=cg.

Flip LHS and RHS.

Defines rule #11.