Certificate for #3805 ⟨a, b | abbaabaaab=a⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(b) = deg(d) = 0, b < d; deg(c) = 1; deg(e) = deg(a) = 2, e < a
• Auxiliary generators:
  1. ab=c
  2. ac=d
  3. bdada=e

Axiom: abbaabaaab=a.

Referenced by [5].

Axiom: ab=c.

Referenced by [5], [10], [16].

Axiom: ac=d.

Referenced by [5], [6], [7], [17], [19].

Axiom: bdada=e.

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

Overlap of [1] abbaabaaab=a with [2] ab=c:

Critical pair: cbaabaaab=a.

Reduce LHS:

Referenced by [6], [8], [11], [13].

Overlap of [3] ac=d with [5] cbdad=a:

Critical pair: aa=dbdad.

Referenced by [8].

Overlap of [4] bdada=e with [3] ac=d:

Critical pair: bdadd=ec.

Referenced by [11], [14].

Overlap of [5] cbdad=a with [4] bdada=e:

Critical pair: ce=aa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [8] dbdad=ce with [4] bdada=e:

Critical pair: de=cea.

Flip LHS and RHS.

Referenced by [10].

Overlap of [9] cea=de with [2] ab=c:

Critical pair: cec=deb.

Referenced by [11].

Overlap of [5] cbdad=a with [7] bdadd=ec:

Critical pair: cec=ad.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [4] bdada=e with [11] ad=deb:

Critical pair: bddeba=e.

Referenced by [18].

Overlap of [5] cbdad=a with [11] ad=deb:

Critical pair: cbddeb=a.

Flip LHS and RHS.

Defines rule #10.

Referenced by [14], [15], [16], [17], [18], [19].

Overlap of [7] bdadd=ec with [13] a=cbddeb:

Critical pair: bdcbddebdd=ec.

Flip LHS and RHS.

Referenced by [22], [28].

Overlap of [11] ad=deb with [13] a=cbddeb:

Critical pair: cbddebd=deb.

Defines rule #7.

Referenced by [22], [28], [30], [32].

Overlap of [2] ab=c with [13] a=cbddeb:

Critical pair: cbddebb=c.

Defines rule #6.

Referenced by [19], [20], [24].

Overlap of [3] ac=d with [13] a=cbddeb:

Critical pair: cbddebc=d.

Referenced by [19], [23].

Simplify [12] bddeba=e.

Reduce LHS:

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

Overlap of [3] ac=d with [16] cbddebb=c:

Critical pair: ac=dbddebb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [18] bddebcbddeb=e with [16] cbddebb=c:

Critical pair: bddebc=eb.

Defines rule #9.

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

Overlap of [18] bddebcbddeb=e with [20] bddebc=eb:

Critical pair: ebbddeb=e.

Defines rule #15.

Referenced by [24], [25], [26], [27], [30], [31].

Overlap of [18] bddebcbddeb=e with [20] bddebc=eb:

Critical pair: bddebceb=ec.

Reduce LHS:

Reduce RHS:

Defines rule #12.

Referenced by [31], [32].

Simplify [17] cbddebc=d.

Reduce LHS:

Defines rule #3.

Referenced by [25], [29].

Overlap of [16] cbddebb=c with [21] ebbddeb=e:

Critical pair: cbdde=cddeb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [30].

Overlap of [23] ceb=d with [21] ebbddeb=e:

Critical pair: ce=dbddeb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [31], [32].

Overlap of [19] dbddebb=d with [21] ebbddeb=e:

Critical pair: dbdde=dddeb.

Flip LHS and RHS.

Defines rule #1.

Overlap of [21] ebbddeb=e with [21] ebbddeb=e:

Critical pair: ebbdde=ebddeb.

Flip LHS and RHS.

Defines rule #14.

Simplify [14] ec=bdcbddebdd.

Reduce RHS:

Defines rule #8.

Referenced by [29].

Overlap of [28] ec=bddebd with [23] ceb=d:

Critical pair: ed=bddebdeb.

Flip LHS and RHS.

Referenced by [33].

Overlap of [24] cddeb=cbdde with [21] ebbddeb=e:

Critical pair: cdde=cbddebddeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [32], [33].

Overlap of [21] ebbddeb=e with [22] ebeb=bddebd:

Critical pair: ebbddbddebd=eeb.

Reduce LHS:

Referenced by [34].

Overlap of [15] cbddebd=deb with [30] debdeb=cdde:

Critical pair: cbdcdde=debeb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [29] bddebdeb=ed with [30] debdeb=cdde:

Critical pair: bdcdde=ed.

Flip LHS and RHS.

Defines rule #5.

Overlap of [31] ebbdced=eeb with [32] ced=cbdcdde:

Critical pair: ebbdcbdcdde=eeb.

Flip LHS and RHS.

Defines rule #11.