Certificate for #4850 ⟨a, b | ababbbba=bab⟩

Completion settings:

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

Axiom: ababbbba=bab.

Referenced by [3].

Axiom: abbbba=c.

Defines rule #10.

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

Overlap of [1] ababbbba=bab with [2] abbbba=c:

Critical pair: abc=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5], [6], [7], [8], [10], [11], [12], [13], [16], [18], [20], [28], [32].

Overlap of [3] bab=abc with [3] bab=abc:

Critical pair: baabc=abcab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [8], [9], [17], [21], [24], [29], [32].

Overlap of [2] abbbba=c with [3] bab=abc:

Critical pair: abbbabc=cb.

Reduce LHS:

Defines rule #1.

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

Overlap of [3] bab=abc with [2] abbbba=c:

Critical pair: bc=abcbbba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [7].

Overlap of [3] bab=abc with [6] abcbbba=bc:

Critical pair: bbc=abccbbba.

Flip LHS and RHS.

Defines rule #13.

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

Overlap of [3] bab=abc with [4] abcab=baabc:

Critical pair: bbaabc=abccab.

Defines rule #5.

Referenced by [12], [14], [18], [19].

Overlap of [4] abcab=baabc with [4] abcab=baabc:

Critical pair: abcbaabc=baabccab.

Defines rule #7.

Overlap of [3] bab=abc with [7] abccbbba=bbc:

Critical pair: bbbc=abcccbbba.

Flip LHS and RHS.

Defines rule #16.

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

Overlap of [7] abccbbba=bbc with [3] bab=abc:

Critical pair: abccbbabc=bbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

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

Overlap of [7] abccbbba=bbc with [8] bbaabc=abccab:

Critical pair: abccbabccab=bbcabc.

Reduce LHS:

Defines rule #8.

Referenced by [24], [25], [26], [30], [33], [34].

Overlap of [3] bab=abc with [11] bbcb=abccabccc:

Critical pair: baabccabccc=abcbcb.

Flip LHS and RHS.

Defines rule #6.

Overlap of [11] bbcb=abccabccc with [8] bbaabc=abccab:

Critical pair: bbcabccab=abccabcccbaabc.

Flip LHS and RHS.

Defines rule #15.

Overlap of [11] bbcb=abccabccc with [11] bbcb=abccabccc:

Critical pair: bbcabccabccc=abccabcccbcb.

Flip LHS and RHS.

Defines rule #14.

Overlap of [3] bab=abc with [10] abcccbbba=bbbc:

Critical pair: bbbbc=abccccbbba.

Flip LHS and RHS.

Defines rule #17.

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

Overlap of [4] abcab=baabc with [10] abcccbbba=bbbc:

Critical pair: abcbbbc=baabccccbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19], [27].

Overlap of [10] abcccbbba=bbbc with [8] bbaabc=abccab:

Critical pair: abcccbabccab=bbbcabc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [27].

Overlap of [8] bbaabc=abccab with [17] bcbbbba=abcbbbc:

Critical pair: bbaaabcbbbc=abccabbbbba.

Flip LHS and RHS.

Defines rule #23.

Referenced by [28], [29], [30].

Overlap of [3] bab=abc with [16] abccccbbba=bbbbc:

Critical pair: bbbbbc=abcccccbbba.

Defines rule #19.

Overlap of [4] abcab=baabc with [16] abccccbbba=bbbbc:

Critical pair: abcbbbbc=baabcccccbbba.

Reduce RHS:

Defines rule #20.

Overlap of [5] aabcccc=cb with [16] abccccbbba=bbbbc:

Critical pair: abbbbc=cbbbba.

Flip LHS and RHS.

Defines rule #18.

Referenced by [23].

Overlap of [5] aabcccc=cb with [22] cbbbba=abbbbc:

Critical pair: aabcccabbbbc=cbbbbba.

Defines rule #22.

Overlap of [4] abcab=baabc with [12] abccabcccab=bbcabc:

Critical pair: abcbbcabc=baabcccabcccab.

Defines rule #12.

Overlap of [12] abccabcccab=bbcabc with [12] abccabcccab=bbcabc:

Critical pair: abccabcccbbcabc=bbcabcccabcccab.

Defines rule #21.

Overlap of [12] abccabcccab=bbcabc with [16] abccccbbba=bbbbc:

Critical pair: abccabcccbbbbc=bbcabcccccbbba.

Defines rule #24.

Overlap of [18] bbbcabc=abcccabcccab with [17] bcbbbba=abcbbbc:

Critical pair: bbbcaabcbbbc=abcccabcccabbbbba.

Flip LHS and RHS.

Defines rule #27.

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

Overlap of [3] bab=abc with [19] abccabbbbba=bbaaabcbbbc:

Critical pair: bbbaaabcbbbc=abcccabbbbba.

Defines rule #25.

Referenced by [31].

Overlap of [4] abcab=baabc with [19] abccabbbbba=bbaaabcbbbc:

Critical pair: abcbbaaabcbbbc=baabcccabbbbba.

Defines rule #26.

Overlap of [12] abccabcccab=bbcabc with [19] abccabbbbba=bbaaabcbbbc:

Critical pair: abccabcccbbaaabcbbbc=bbcabcccabbbbba.

Defines rule #31.

Overlap of [16] abccccbbba=bbbbc with [28] bbbaaabcbbbc=abcccabbbbba:

Critical pair: abccccabcccabbbbba=bbbbcaabcbbbc.

Flip LHS and RHS.

Defines rule #28.

Overlap of [4] abcab=baabc with [27] abcccabcccabbbbba=bbbcaabcbbbc:

Critical pair: abcbbbcaabcbbbc=baabccccabcccabbbbba.

Reduce RHS:

Defines rule #29.

Overlap of [12] abccabcccab=bbcabc with [27] abcccabcccabbbbba=bbbcaabcbbbc:

Critical pair: abccbbbcaabcbbbc=bbcabccccabbbbba.

Defines rule #30.

Overlap of [12] abccabcccab=bbcabc with [27] abcccabcccabbbbba=bbbcaabcbbbc:

Critical pair: abccabcccbbbcaabcbbbc=bbcabccccabcccabbbbba.

Defines rule #32.