Certificate for #5378 ⟨a, b | ababbba=bbab⟩

Completion settings:

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

Axiom: ababbba=bbab.

Referenced by [3].

Axiom: abbba=c.

Defines rule #2.

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

Overlap of [1] ababbba=bbab with [2] abbba=c:

Critical pair: abc=bbab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [6], [7], [8], [9], [10], [15], [18].

Overlap of [2] abbba=c with [2] abbba=c:

Critical pair: abbbc=cbbba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [13], [14], [16], [22], [23], [24], [25], [26], [31], [35], [36], [37], [39], [40], [41], [42], [43], [44], [45], [46].

Overlap of [2] abbba=c with [3] bbab=abc:

Critical pair: ababc=cb.

Defines rule #3.

Referenced by [8], [11], [13], [19].

Overlap of [3] bbab=abc with [2] abbba=c:

Critical pair: bbc=abcbba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [9].

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

Critical pair: bbaabc=abcbab.

Flip LHS and RHS.

Defines rule #5.

Referenced by [15], [16], [17], [20], [22], [26], [27], [31], [35].

Overlap of [3] bbab=abc with [5] ababc=cb:

Critical pair: bbcb=abcabc.

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [11], [12], [14], [17], [21].

Overlap of [3] bbab=abc with [6] abcbba=bbc:

Critical pair: bbbbc=abccbba.

Flip LHS and RHS.

Defines rule #9.

Referenced by [18], [19], [20], [21], [32].

Overlap of [3] bbab=abc with [8] abcabc=bbcb:

Critical pair: bbbbcb=abccabc.

Defines rule #13.

Referenced by [23], [28], [36].

Overlap of [5] ababc=cb with [8] abcabc=bbcb:

Critical pair: abbbcb=cbabc.

Defines rule #8.

Referenced by [24], [29], [37].

Overlap of [8] abcabc=bbcb with [8] abcabc=bbcb:

Critical pair: abcbbcb=bbcbabc.

Defines rule #14.

Referenced by [30].

Overlap of [5] ababc=cb with [4] cbbba=abbbc:

Critical pair: abababbbc=cbbbba.

Defines rule #12.

Overlap of [8] abcabc=bbcb with [4] cbbba=abbbc:

Critical pair: abcababbbc=bbcbbbba.

Defines rule #18.

Overlap of [3] bbab=abc with [7] abcbab=bbaabc:

Critical pair: bbbbaabc=abccbab.

Defines rule #10.

Referenced by [22], [23], [24], [25].

Overlap of [7] abcbab=bbaabc with [7] abcbab=bbaabc:

Critical pair: abcbbbaabc=bbaabccbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [27], [28], [29], [30], [31], [32], [33], [34], [38].

Overlap of [7] abcbab=bbaabc with [8] abcabc=bbcb:

Critical pair: abcbbbcb=bbaabccabc.

Defines rule #19.

Referenced by [26], [34].

Overlap of [3] bbab=abc with [9] abccbba=bbbbc:

Critical pair: bbbbbbc=abcccbba.

Defines rule #15.

Overlap of [5] ababc=cb with [9] abccbba=bbbbc:

Critical pair: abbbbbc=cbcbba.

Defines rule #11.

Overlap of [7] abcbab=bbaabc with [9] abccbba=bbbbc:

Critical pair: abcbbbbbc=bbaabcccbba.

Defines rule #20.

Overlap of [8] abcabc=bbcb with [9] abccbba=bbbbc:

Critical pair: abcbbbbc=bbcbcbba.

Defines rule #17.

Overlap of [7] abcbab=bbaabc with [15] bbbbaabc=abccbab:

Critical pair: abcbaabccbab=bbaabcbbbaabc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [10] bbbbcb=abccabc with [15] bbbbaabc=abccbab:

Critical pair: bbbbcabccbab=abccabcbbbaabc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [11] abbbcb=cbabc with [15] bbbbaabc=abccbab:

Critical pair: abbbcabccbab=cbabcbbbaabc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [15] bbbbaabc=abccbab with [4] cbbba=abbbc:

Critical pair: bbbbaababbbc=abccbabbbba.

Defines rule #21.

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

Overlap of [7] abcbab=bbaabc with [17] abcbbbcb=bbaabccabc:

Critical pair: abcbbbaabccabc=bbaabccbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [38].

Overlap of [7] abcbab=bbaabc with [16] bbaabccbab=ababbbcabc:

Critical pair: abcbaababbbcabc=bbaabcbaabccbab.

Defines rule #26.

Referenced by [41].

Overlap of [10] bbbbcb=abccabc with [16] bbaabccbab=ababbbcabc:

Critical pair: bbbbcababbbcabc=abccabcbaabccbab.

Defines rule #31.

Referenced by [42].

Overlap of [11] abbbcb=cbabc with [16] bbaabccbab=ababbbcabc:

Critical pair: abbbcababbbcabc=cbabcbaabccbab.

Defines rule #28.

Referenced by [40].

Overlap of [12] abcbbcb=bbcbabc with [16] bbaabccbab=ababbbcabc:

Critical pair: abcbbcababbbcabc=bbcbabcbaabccbab.

Defines rule #32.

Referenced by [43].

Overlap of [16] bbaabccbab=ababbbcabc with [7] abcbab=bbaabc:

Critical pair: bbaabccbbbaabc=ababbbcabccbab.

Reduce LHS:

Defines rule #24.

Referenced by [39].

Overlap of [16] bbaabccbab=ababbbcabc with [9] abccbba=bbbbc:

Critical pair: bbaabccbbbbbc=ababbbcabcccbba.

Defines rule #29.

Overlap of [16] bbaabccbab=ababbbcabc with [16] bbaabccbab=ababbbcabc:

Critical pair: bbaabccbaababbbcabc=ababbbcabcbaabccbab.

Defines rule #35.

Referenced by [45].

Overlap of [17] abcbbbcb=bbaabccabc with [16] bbaabccbab=ababbbcabc:

Critical pair: abcbbbcababbbcabc=bbaabccabcbaabccbab.

Defines rule #37.

Referenced by [44].

Overlap of [7] abcbab=bbaabc with [25] bbbbaababbbc=abccbabbbba:

Critical pair: abcbaabccbabbbba=bbaabcbbbaababbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #30.

Overlap of [10] bbbbcb=abccabc with [25] bbbbaababbbc=abccbabbbba:

Critical pair: bbbbcabccbabbbba=abccabcbbbaababbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #38.

Overlap of [11] abbbcb=cbabc with [25] bbbbaababbbc=abccbabbbba:

Critical pair: abbbcabccbabbbba=cbabcbbbaababbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #33.

Overlap of [26] bbaabccbbbcb=ababbbcabccabc with [16] bbaabccbab=ababbbcabc:

Critical pair: bbaabccbbbcababbbcabc=ababbbcabccabcbaabccbab.

Defines rule #43.

Referenced by [46].

Overlap of [31] bbaabcabbbcabc=ababbbcabccbab with [4] cbbba=abbbc:

Critical pair: bbaabcabbbcababbbc=ababbbcabccbabbbba.

Defines rule #34.

Overlap of [29] abbbcababbbcabc=cbabcbaabccbab with [4] cbbba=abbbc:

Critical pair: abbbcababbbcababbbc=cbabcbaabccbabbbba.

Defines rule #39.

Overlap of [27] abcbaababbbcabc=bbaabcbaabccbab with [4] cbbba=abbbc:

Critical pair: abcbaababbbcababbbc=bbaabcbaabccbabbbba.

Defines rule #36.

Overlap of [28] bbbbcababbbcabc=abccabcbaabccbab with [4] cbbba=abbbc:

Critical pair: bbbbcababbbcababbbc=abccabcbaabccbabbbba.

Defines rule #40.

Overlap of [30] abcbbcababbbcabc=bbcbabcbaabccbab with [4] cbbba=abbbc:

Critical pair: abcbbcababbbcababbbc=bbcbabcbaabccbabbbba.

Defines rule #41.

Overlap of [34] abcbbbcababbbcabc=bbaabccabcbaabccbab with [4] cbbba=abbbc:

Critical pair: abcbbbcababbbcababbbc=bbaabccabcbaabccbabbbba.

Defines rule #44.

Overlap of [33] bbaabccbaababbbcabc=ababbbcabcbaabccbab with [4] cbbba=abbbc:

Critical pair: bbaabccbaababbbcababbbc=ababbbcabcbaabccbabbbba.

Defines rule #42.

Overlap of [38] bbaabccbbbcababbbcabc=ababbbcabccabcbaabccbab with [4] cbbba=abbbc:

Critical pair: bbaabccbbbcababbbcababbbc=ababbbcabccabcbaabccbabbbba.

Defines rule #45.