Certificate for #2249 ⟨a, b | aababba=baa⟩

Completion settings:

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

Axiom: aababba=baa.

Referenced by [5].

Axiom: aababb=c.

Referenced by [5], [6].

Axiom: bc=d.

Defines rule #31.

Referenced by [7], [9], [11], [13], [14], [16], [26], [36].

Axiom: babb=e.

Defines rule #41.

Referenced by [6], [11], [12], [13], [14], [15], [16].

Overlap of [1] aababba=baa with [2] aababb=c:

Critical pair: ca=baa.

Flip LHS and RHS.

Defines rule #33.

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

Overlap of [2] aababb=c with [4] babb=e:

Critical pair: aae=c.

Defines rule #7.

Referenced by [7], [8], [17], [19], [21], [31], [40].

Overlap of [5] baa=ca with [6] aae=c:

Critical pair: bc=cae.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [9], [10], [18], [20], [22], [31].

Overlap of [5] baa=ca with [6] aae=c:

Critical pair: bac=caae.

Reduce RHS:

Defines rule #34.

Referenced by [10], [14], [27], [37].

Overlap of [3] bc=d with [7] cae=d:

Critical pair: bd=dae.

Defines rule #32.

Referenced by [11], [15].

Overlap of [8] bac=cc with [7] cae=d:

Critical pair: bad=ccae.

Reduce RHS:

Defines rule #35.

Referenced by [11], [13], [14], [15], [16].

Overlap of [4] babb=e with [3] bc=d:

Critical pair: babd=ec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [23], [24], [25], [28], [30], [38].

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

Critical pair: babe=eabb.

Defines rule #40.

Overlap of [4] babb=e with [5] baa=ca:

Critical pair: babca=eaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [17], [18], [33].

Overlap of [4] babb=e with [8] bac=cc:

Critical pair: babcc=eac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [19], [20], [23], [24], [25], [29], [30], [34], [39].

Overlap of [4] babb=e with [9] bd=dae:

Critical pair: babdae=ed.

Reduce LHS:

Defines rule #20.

Referenced by [26], [27], [28], [29], [30], [31], [32], [34], [35], [40].

Overlap of [4] babb=e with [10] bad=cd:

Critical pair: babcd=ead.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [21], [22].

Overlap of [6] aae=c with [13] eaa=cda:

Critical pair: aacda=caa.

Defines rule #1.

Overlap of [7] cae=d with [13] eaa=cda:

Critical pair: cacda=daa.

Defines rule #2.

Referenced by [23], [31], [40].

Overlap of [6] aae=c with [14] eac=cdc:

Critical pair: aacdc=cac.

Defines rule #3.

Referenced by [31], [40].

Overlap of [7] cae=d with [14] eac=cdc:

Critical pair: cacdc=dac.

Defines rule #4.

Referenced by [24], [32], [41].

Overlap of [6] aae=c with [16] ead=cdd:

Critical pair: aacdd=cad.

Defines rule #5.

Overlap of [7] cae=d with [16] ead=cdd:

Critical pair: cacdd=dad.

Defines rule #6.

Referenced by [25].

Overlap of [11] ec=cdae with [18] cacda=daa:

Critical pair: edaa=cdaeacda.

Reduce RHS:

Defines rule #17.

Overlap of [11] ec=cdae with [20] cacdc=dac:

Critical pair: edac=cdaeacdc.

Reduce RHS:

Defines rule #18.

Referenced by [42].

Overlap of [11] ec=cdae with [22] cacdd=dad:

Critical pair: edad=cdaeacdd.

Reduce RHS:

Defines rule #19.

Overlap of [3] bc=d with [15] cdaeae=ed:

Critical pair: bed=ddaeae.

Defines rule #36.

Overlap of [8] bac=cc with [15] cdaeae=ed:

Critical pair: baed=ccdaeae.

Reduce RHS:

Defines rule #37.

Overlap of [11] ec=cdae with [15] cdaeae=ed:

Critical pair: eed=cdaedaeae.

Flip LHS and RHS.

Defines rule #26.

Referenced by [35], [36], [37], [38], [39], [40], [41], [42], [43].

Overlap of [14] eac=cdc with [15] cdaeae=ed:

Critical pair: eaed=cdcdaeae.

Reduce RHS:

Defines rule #23.

Referenced by [34].

Overlap of [15] cdaeae=ed with [11] ec=cdae:

Critical pair: cdaeacdae=edc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [35], [43].

Overlap of [19] aacdc=cac with [15] cdaeae=ed:

Critical pair: aacded=cacdaeae.

Reduce RHS:

Defines rule #10.

Referenced by [33].

Overlap of [20] cacdc=dac with [15] cdaeae=ed:

Critical pair: cacded=dacdaeae.

Reduce RHS:

Defines rule #11.

Overlap of [13] eaa=cda with [31] aacded=dd:

Critical pair: edd=cdacded.

Defines rule #16.

Overlap of [15] cdaeae=ed with [29] eaed=cded:

Critical pair: cdaeacded=edaed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [38], [43].

Overlap of [30] edc=cdacdcdae with [15] cdaeae=ed:

Critical pair: eded=cdacdcdaedaeae.

Reduce RHS:

Defines rule #24.

Overlap of [3] bc=d with [28] cdaedaeae=eed:

Critical pair: beed=ddaedaeae.

Defines rule #38.

Overlap of [8] bac=cc with [28] cdaedaeae=eed:

Critical pair: baeed=ccdaedaeae.

Reduce RHS:

Defines rule #39.

Overlap of [11] ec=cdae with [28] cdaedaeae=eed:

Critical pair: eeed=cdaedaedaeae.

Reduce RHS:

Defines rule #27.

Overlap of [14] eac=cdc with [28] cdaedaeae=eed:

Critical pair: eaeed=cdcdaedaeae.

Reduce RHS:

Defines rule #28.

Overlap of [19] aacdc=cac with [28] cdaedaeae=eed:

Critical pair: aacdeed=cacdaedaeae.

Reduce RHS:

Defines rule #21.

Overlap of [20] cacdc=dac with [28] cdaedaeae=eed:

Critical pair: cacdeed=dacdaedaeae.

Reduce RHS:

Defines rule #22.

Overlap of [24] edac=cdacdcdc with [28] cdaedaeae=eed:

Critical pair: edaeed=cdacdcdcdaedaeae.

Reduce RHS:

Defines rule #30.

Overlap of [30] edc=cdacdcdae with [28] cdaedaeae=eed:

Critical pair: edeed=cdacdcdaedaedaeae.

Reduce RHS:

Defines rule #29.