Certificate for #11590 ⟨a, b | baaab=a, bbbbb=1⟩

Completion settings:

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

Axiom: baaab=a.

Referenced by [4], [5], [6], [7], [8], [9], [10], [13], [15], [16], [27].

Axiom: bbbbb=1.

Defines rule #19.

Referenced by [5], [6].

Axiom: baabaabaabaab=c.

Referenced by [12], [13], [14], [15], [16], [17].

Overlap of [1] baaab=a with [1] baaab=a:

Critical pair: baaaa=aaaab.

Flip LHS and RHS.

Referenced by [11], [15], [20].

Overlap of [1] baaab=a with [2] bbbbb=1:

Critical pair: baaa=abbbb.

Flip LHS and RHS.

Referenced by [8].

Overlap of [2] bbbbb=1 with [1] baaab=a:

Critical pair: bbbba=aaab.

Referenced by [7], [14].

Overlap of [6] bbbba=aaab with [1] baaab=a:

Critical pair: bbba=aaabaab.

Referenced by [9], [30].

Overlap of [1] baaab=a with [5] abbbb=baaa:

Critical pair: baabaaa=abbb.

Flip LHS and RHS.

Referenced by [10], [11], [15], [29], [31].

Overlap of [7] bbba=aaabaab with [1] baaab=a:

Critical pair: bba=aaabaabaab.

Flip LHS and RHS.

Referenced by [16].

Overlap of [1] baaab=a with [8] abbb=baabaaa:

Critical pair: baabaabaaa=abb.

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

Overlap of [8] abbb=baabaaa with [10] baabaabaaa=abb:

Critical pair: abbabb=baabaaaaabaabaaa.

Reduce RHS:

Referenced by [32].

Overlap of [3] baabaabaabaab=c with [3] baabaabaabaab=c:

Critical pair: baac=caab.

Flip LHS and RHS.

Referenced by [22].

Overlap of [3] baabaabaabaab=c with [10] baabaabaaa=abb:

Critical pair: baabaaabb=caaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [20], [21], [25], [27], [28].

Overlap of [6] bbbba=aaab with [3] baabaabaabaab=c:

Critical pair: bbbc=aaababaabaabaab.

Flip LHS and RHS.

Referenced by [19].

Overlap of [8] abbb=baabaaa with [3] baabaabaabaab=c:

Critical pair: abbc=baabaaaaabaabaabaab.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [9] aaabaabaab=bba with [3] baabaabaabaab=c:

Critical pair: aaac=bbaaabaab.

Reduce RHS:

Referenced by [21], [23], [28], [30], [32].

Overlap of [3] baabaabaabaab=c with [15] baabaaba=abbc:

Critical pair: abbcabaab=c.

Referenced by [33].

Overlap of [10] baabaabaaa=abb with [15] baabaaba=abbc:

Critical pair: abbcaa=abb.

Defines rule #11.

Overlap of [14] aaababaabaabaab=bbbc with [15] baabaaba=abbc:

Critical pair: aaabaabbcab=bbbc.

Referenced by [34].

Overlap of [13] caaa=a with [4] aaaab=baaaa:

Critical pair: cbaaaa=aab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [22], [25], [29], [30], [31], [32], [34], [35], [36], [38].

Overlap of [13] caaa=a with [16] aaac=a:

Critical pair: ca=ac.

Flip LHS and RHS.

Defines rule #1.

Referenced by [22], [23], [24], [25], [26], [28], [30], [33], [34], [37], [40], [46].

Simplify [12] caab=baac.

Reduce LHS:

Reduce RHS:

Referenced by [23], [24].

Overlap of [22] ccbaaaa=bcaa with [16] aaac=a:

Critical pair: ccbaa=bcaac.

Reduce RHS:

Referenced by [27], [28].

Overlap of [21] ac=ca with [22] ccbaaaa=bcaa:

Critical pair: abcaa=cacbaaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [13] caaa=a with [20] aab=cbaaaa:

Critical pair: cacbaaaa=ab.

Reduce LHS:

Defines rule #5.

Referenced by [26], [34].

Overlap of [25] abcaa=ab with [21] ac=ca:

Critical pair: abcaca=abc.

Reduce LHS:

Referenced by [33].

Overlap of [23] ccbaa=bccaa with [1] baaab=a:

Critical pair: cca=bccaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [29], [33], [34].

Overlap of [23] ccbaa=bccaa with [16] aaac=a:

Critical pair: ccba=bccaaac.

Reduce RHS:

Referenced by [35], [36], [37], [38].

Overlap of [27] bcab=cca with [8] abbb=baabaaa:

Critical pair: bcbaabaaa=ccabb.

Reduce LHS:

Referenced by [41].

Simplify [7] bbba=aaabaab.

Reduce RHS:

Defines rule #13.

Simplify [8] abbb=baabaaa.

Reduce RHS:

Defines rule #16.

Simplify [11] abbabb=baababaabaaaaaaa.

Reduce RHS:

Defines rule #17.

Overlap of [17] abbcabaab=c with [27] bcab=cca:

Critical pair: abccaaab=c.

Reduce LHS:

Defines rule #2.

Referenced by [35], [36], [38], [39], [42], [43], [44].

Overlap of [19] aaabaabbcab=bbbc with [27] bcab=cca:

Critical pair: aaabaabcca=bbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [38].

Overlap of [33] ccaa=c with [20] aab=cbaaaa:

Critical pair: cccbaaaa=cb.

Reduce LHS:

Defines rule #4.

Referenced by [36], [39], [42], [44], [45], [46].

Overlap of [35] cbcaa=cb with [20] aab=cbaaaa:

Critical pair: cbccbaaaa=cbb.

Reduce LHS:

Defines rule #10.

Referenced by [38].

Overlap of [28] ccba=bcca with [21] ac=ca:

Critical pair: ccbca=bccac.

Reduce RHS:

Referenced by [39].

Overlap of [36] cbbcaa=cbb with [20] aab=cbaaaa:

Critical pair: cbbccbaaaa=cbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [37] ccbca=bccca with [35] cbcaa=cb:

Critical pair: ccb=bcccaa.

Reduce RHS:

Defines rule #6.

Referenced by [40], [41], [42], [43], [44].

Overlap of [21] ac=ca with [39] ccb=bcc:

Critical pair: abcc=cacb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [41], [42], [43], [44].

Simplify [29] bcbcbaaaaaaa=ccabb.

Reduce RHS:

Referenced by [42].

Overlap of [39] ccb=bcc with [41] bcbcbaaaaaaa=abbcc:

Critical pair: ccabbcc=bcccbcbaaaaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [43].

Overlap of [39] ccb=bcc with [42] bcbcbaaa=abbcccc:

Critical pair: ccabbcccc=bcccbcbaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [45].

Simplify [38] cbbb=ccabcbaaaaaaa.

Reduce RHS:

Defines rule #15.

Referenced by [46].

Overlap of [43] bcbcbca=abbcccccc with [35] cbcaa=cb:

Critical pair: bcbcb=abbcccccca.

Defines rule #14.

Referenced by [46].

Overlap of [44] cbbb=abcbaaa with [45] bcbcb=abbcccccca:

Critical pair: cbbabbcccccca=abcbaaacbcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.