Certificate for #22287 ⟨a, b | aaa=1, abbbba=bb⟩

Completion settings:

• Auxiliary generators:
  1. c = abb
• Reduction order:
  • Left-to-right recursive path with deg(c) = 0; deg(a) = 1; deg(b) = 2

Axiom: aaa=1.

Defines rule #7.

Referenced by [5], [9], [11], [12], [13], [15], [17], [18], [20], [25], [27], [30], [39], [42], [44].

Axiom: abbbba=bb.

Referenced by [4].

Axiom: abb=c.

Referenced by [4], [5], [6].

Overlap of [2] abbbba=bb with [3] abb=c:

Critical pair: cbba=bb.

Referenced by [8].

Overlap of [1] aaa=1 with [3] abb=c:

Critical pair: aac=bb.

Flip LHS and RHS.

Defines rule #22.

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

Overlap of [3] abb=c with [5] bb=aac:

Critical pair: abaac=cb.

Defines rule #16.

Referenced by [10], [11], [19], [21], [26], [30], [32], [34].

Overlap of [5] bb=aac with [5] bb=aac:

Critical pair: baac=aacb.

Flip LHS and RHS.

Defines rule #20.

Referenced by [10], [33], [35], [42].

Simplify [4] cbba=bb.

Reduce LHS:

Reduce RHS:

Referenced by [9], [10], [11], [14], [15], [17].

Overlap of [8] caaca=aac with [1] aaa=1:

Critical pair: caac=aacaa.

Flip LHS and RHS.

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

Overlap of [8] caaca=aac with [6] abaac=cb:

Critical pair: caaccb=aacbaac.

Reduce RHS:

Referenced by [34].

Overlap of [6] abaac=cb with [8] caaca=aac:

Critical pair: abaaaac=cbaaca.

Reduce LHS:

Referenced by [22].

Overlap of [1] aaa=1 with [9] aacaa=caac:

Critical pair: acaac=caa.

Referenced by [16].

Overlap of [1] aaa=1 with [9] aacaa=caac:

Critical pair: aacaac=acaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [8] caaca=aac with [9] aacaa=caac:

Critical pair: ccaac=aaca.

Flip LHS and RHS.

Defines rule #8.

Referenced by [22], [44].

Overlap of [9] aacaa=caac with [8] caaca=aac:

Critical pair: aaaac=caacca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [25], [29].

Simplify [12] acaac=caa.

Reduce LHS:

Defines rule #5.

Referenced by [17], [18], [20], [24], [25], [35].

Overlap of [16] caaccc=caa with [8] caaca=aac:

Critical pair: caaccaac=caaaaca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [25], [26], [39].

Overlap of [16] caaccc=caa with [16] caaccc=caa:

Critical pair: caacccaa=caaaaccc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [19], [20], [23], [28], [31], [33], [36], [38], [40].

Overlap of [6] abaac=cb with [18] caccc=ca:

Critical pair: abaaca=cbaccc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [36].

Overlap of [16] caaccc=caa with [18] caccc=ca:

Critical pair: caaccca=caaaccc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [21], [33], [34], [43].

Overlap of [6] abaac=cb with [20] cccc=c:

Critical pair: abaac=cbccc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [23], [24], [36], [40], [44].

Simplify [11] abac=cbaaca.

Reduce RHS:

Defines rule #15.

Referenced by [44].

Overlap of [18] caccc=ca with [21] cbccc=cb:

Critical pair: cacccb=cabccc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [21] cbccc=cb with [16] caaccc=caa:

Critical pair: cbcccaa=cbaaccc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [45].

Overlap of [16] caaccc=caa with [17] caca=acac:

Critical pair: caaccacac=caaaca.

Reduce LHS:

Reduce RHS:

Referenced by [27], [28].

Overlap of [17] caca=acac with [6] abaac=cb:

Critical pair: caccb=acacbaac.

Flip LHS and RHS.

Referenced by [39].

Overlap of [1] aaa=1 with [25] accac=cca:

Critical pair: aacca=ccac.

Referenced by [29].

Overlap of [25] accac=cca with [18] caccc=ca:

Critical pair: acca=ccacc.

Defines rule #4.

Referenced by [32], [33], [34], [40].

Simplify [15] caacca=ac.

Reduce LHS:

Referenced by [30], [31].

Overlap of [6] abaac=cb with [29] cccac=ac:

Critical pair: abaaac=cbccac.

Reduce LHS:

Defines rule #14.

Referenced by [36], [38].

Overlap of [29] cccac=ac with [18] caccc=ca:

Critical pair: ccca=accc.

Defines rule #3.

Referenced by [34], [42], [43].

Overlap of [28] acca=ccacc with [6] abaac=cb:

Critical pair: acccb=ccaccbaac.

Flip LHS and RHS.

Referenced by [40].

Overlap of [28] acca=ccacc with [7] aacb=baac:

Critical pair: accbaac=ccaccacb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [37], [41].

Overlap of [13] acaa=caacc with [6] abaac=cb:

Critical pair: acacb=caaccbaac.

Reduce RHS:

Referenced by [39], [44].

Overlap of [13] acaa=caacc with [7] aacb=baac:

Critical pair: acbaac=caacccb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [19] cbaccc=cba with [21] cbccc=cb:

Critical pair: cbacccb=cbabccc.

Reduce LHS:

Reduce RHS:

Defines rule #23.

Simplify [23] cabccc=cab.

Reduce RHS:

Referenced by [38].

Overlap of [37] cabccc=accbaac with [30] abc=cbccac:

Critical pair: ccbccaccc=accbaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [26] acacbaac=caccb with [34] acacb=bacac:

Critical pair: bacacaac=caccb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [40], [43].

Overlap of [32] ccaccbaac=acccb with [39] caccb=bcacc:

Critical pair: cbcaccaac=acccb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [42], [45].

Simplify [33] cab=accbaac.

Reduce RHS:

Defines rule #18.

Overlap of [1] aaa=1 with [40] acccb=cbcca:

Critical pair: aacbcca=cccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [31] ccca=accc with [39] caccb=bcacc:

Critical pair: ccbcacc=acccccb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [1] aaa=1 with [34] acacb=bacac:

Critical pair: aabacac=cacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [24] cbaaccc=cbaa with [40] acccb=cbcca:

Critical pair: cbacbcca=cbaab.

Flip LHS and RHS.

Defines rule #24.