Certificate for #3791 ⟨a, b | ababbbbaab=a⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(c) = 0; deg(a) = 1; deg(b) = 2
• Auxiliary generators:
  1. babbbba=c

Axiom: ababbbbaab=a.

Referenced by [3].

Axiom: babbbba=c.

Defines rule #20.

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

Overlap of [1] ababbbbaab=a with [2] babbbba=c:

Critical pair: acab=a.

Defines rule #9.

Referenced by [5], [6], [8], [10], [12], [14], [16], [18].

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

Critical pair: babbbc=cbbbba.

Flip LHS and RHS.

Defines rule #17.

Overlap of [2] babbbba=c with [3] acab=a:

Critical pair: babbbba=ccab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [7], [9], [11], [13], [15].

Overlap of [3] acab=a with [2] babbbba=c:

Critical pair: acac=aabbbba.

Flip LHS and RHS.

Defines rule #19.

Overlap of [5] ccab=c with [2] babbbba=c:

Critical pair: ccac=cabbbba.

Flip LHS and RHS.

Defines rule #18.

Referenced by [8], [9].

Overlap of [3] acab=a with [7] cabbbba=ccac:

Critical pair: accac=abbba.

Flip LHS and RHS.

Defines rule #16.

Referenced by [10], [11].

Overlap of [5] ccab=c with [7] cabbbba=ccac:

Critical pair: cccac=cbbba.

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] acab=a with [8] abbba=accac:

Critical pair: acaccac=abba.

Flip LHS and RHS.

Defines rule #14.

Referenced by [12], [13].

Overlap of [5] ccab=c with [8] abbba=accac:

Critical pair: ccaccac=cbba.

Flip LHS and RHS.

Defines rule #13.

Overlap of [3] acab=a with [10] abba=acaccac:

Critical pair: acacaccac=aba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [14], [15].

Overlap of [5] ccab=c with [10] abba=acaccac:

Critical pair: ccacaccac=cba.

Flip LHS and RHS.

Defines rule #11.

Overlap of [3] acab=a with [12] aba=acacaccac:

Critical pair: acacacaccac=aa.

Defines rule #5.

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

Overlap of [5] ccab=c with [12] aba=acacaccac:

Critical pair: ccacacaccac=ca.

Defines rule #2.

Referenced by [16], [17], [20], [21].

Overlap of [15] ccacacaccac=ca with [3] acab=a:

Critical pair: ccacacacca=caab.

Flip LHS and RHS.

Defines rule #8.

Overlap of [15] ccacacaccac=ca with [15] ccacacaccac=ca:

Critical pair: ccacacaca=caacaccac.

Flip LHS and RHS.

Defines rule #1.

Overlap of [14] acacacaccac=aa with [3] acab=a:

Critical pair: acacacacca=aaab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [14] acacacaccac=aa with [14] acacacaccac=aa:

Critical pair: acacacaccaa=aaacacaccac.

Flip LHS and RHS.

Defines rule #6.

Overlap of [14] acacacaccac=aa with [15] ccacacaccac=ca:

Critical pair: acacacaca=aaacaccac.

Flip LHS and RHS.

Defines rule #3.

Overlap of [15] ccacacaccac=ca with [14] acacacaccac=aa:

Critical pair: ccacacaccaa=caacacaccac.

Flip LHS and RHS.

Defines rule #4.