Certificate for #5657 ⟨a, b | aabaab=abbaa⟩

Completion settings:

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

Axiom: aabaab=abbaa.

Flip LHS and RHS.

Referenced by [5].

Axiom: aaba=c.

Referenced by [5], [7].

Axiom: ab=d.

Defines rule #16.

Referenced by [5], [6], [7], [8], [10].

Axiom: db=e.

Defines rule #17.

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

Simplify [1] abbaa=aabaab.

Reduce RHS:

Referenced by [6].

Overlap of [5] abbaa=cd with [3] ab=d:

Critical pair: dbaa=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [9], [10], [13], [16].

Overlap of [2] aaba=c with [3] ab=d:

Critical pair: ada=c.

Defines rule #6.

Referenced by [8], [9], [12], [14], [21].

Overlap of [7] ada=c with [3] ab=d:

Critical pair: add=cb.

Flip LHS and RHS.

Defines rule #14.

Overlap of [7] ada=c with [7] ada=c:

Critical pair: adc=cda.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [15].

Overlap of [6] cd=eaa with [4] db=e:

Critical pair: ce=eaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

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

Overlap of [10] ead=ce with [4] db=e:

Critical pair: eae=ceb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [17].

Overlap of [10] ead=ce with [7] ada=c:

Critical pair: ec=cea.

Flip LHS and RHS.

Defines rule #1.

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

Overlap of [12] cea=ec with [10] ead=ce:

Critical pair: cce=ecd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [14].

Overlap of [13] eeaa=cce with [7] ada=c:

Critical pair: eeac=cceda.

Flip LHS and RHS.

Defines rule #9.

Referenced by [20].

Overlap of [12] cea=ec with [9] eaaa=adc:

Critical pair: cadc=ecaa.

Defines rule #7.

Referenced by [16], [17], [18], [19], [20].

Overlap of [15] cadc=ecaa with [6] cd=eaa:

Critical pair: cadeaa=ecaad.

Defines rule #10.

Referenced by [21].

Overlap of [15] cadc=ecaa with [11] ceb=eae:

Critical pair: cadeae=ecaaeb.

Flip LHS and RHS.

Defines rule #18.

Overlap of [15] cadc=ecaa with [12] cea=ec:

Critical pair: cadec=ecaaea.

Flip LHS and RHS.

Defines rule #8.

Overlap of [15] cadc=ecaa with [15] cadc=ecaa:

Critical pair: cadecaa=ecaaadc.

Defines rule #11.

Overlap of [15] cadc=ecaa with [14] cceda=eeac:

Critical pair: cadeeac=ecaaceda.

Flip LHS and RHS.

Defines rule #12.

Overlap of [16] cadeaa=ecaad with [7] ada=c:

Critical pair: cadeac=ecaadda.

Flip LHS and RHS.

Defines rule #13.