Certificate for #5345 ⟨a, b | ababaab=abba⟩

Completion settings:

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

Axiom: ababaab=abba.

Defines rule #11.

Referenced by [4], [5], [6], [7], [9], [11], [14], [16], [17], [18], [23], [26].

Axiom: abbab=c.

Defines rule #2.

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

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

Critical pair: abbc=cbab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

Overlap of [1] ababaab=abba with [1] ababaab=abba:

Critical pair: ababaabba=abbaabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [11], [12], [13], [14].

Overlap of [1] ababaab=abba with [2] abbab=c:

Critical pair: ababac=abbabab.

Reduce RHS:

Defines rule #4.

Referenced by [7], [8], [10], [11], [13], [15], [16], [19], [20], [24], [27].

Overlap of [2] abbab=c with [1] ababaab=abba:

Critical pair: abbabba=cabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [9], [10], [12], [15].

Overlap of [1] ababaab=abba with [5] ababac=cab:

Critical pair: ababacab=abbaabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [12], [13], [21], [22], [25].

Overlap of [2] abbab=c with [5] ababac=cab:

Critical pair: abbcab=cabac.

Flip LHS and RHS.

Defines rule #3.

Referenced by [10].

Overlap of [6] cabaab=cba with [1] ababaab=abba:

Critical pair: cabaabba=cbaabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [6] cabaab=cba with [5] ababac=cab:

Critical pair: cabacab=cbaabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [1] ababaab=abba with [4] abbaabaab=ca:

Critical pair: ababaca=abbabaabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [14], [15].

Overlap of [4] abbaabaab=ca with [4] abbaabaab=ca:

Critical pair: abbaabaca=cabaabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [16], [21], [22].

Overlap of [4] abbaabaab=ca with [5] ababac=cab:

Critical pair: abbaabacab=caabac.

Reduce LHS:

Defines rule #6.

Referenced by [17], [18], [19], [20], [21], [22], [25].

Overlap of [11] caabaab=caba with [4] abbaabaab=ca:

Critical pair: caabaca=cababaabaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [11] caabaab=caba with [5] ababac=cab:

Critical pair: caabacab=cabaabac.

Reduce RHS:

Defines rule #14.

Referenced by [18], [20], [21], [23], [24].

Overlap of [12] cbaaab=cababa with [5] ababac=cab:

Critical pair: cbaacab=cababaabac.

Reduce RHS:

Defines rule #9.

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

Overlap of [13] cababab=caabac with [1] ababaab=abba:

Critical pair: cababba=caabacaab.

Flip LHS and RHS.

Defines rule #22.

Referenced by [22].

Overlap of [13] cababab=caabac with [1] ababaab=abba:

Critical pair: cabababba=caabacabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [13] cababab=caabac with [5] ababac=cab:

Critical pair: cabcab=caabacac.

Flip LHS and RHS.

Defines rule #15.

Overlap of [13] cababab=caabac with [5] ababac=cab:

Critical pair: cababcab=caabacabac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [7] abbaabac=cabab with [12] cbaaab=cababa:

Critical pair: abbaabacababa=cababbaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [12] cbaaab=cababa with [7] abbaabac=cabab:

Critical pair: cbaacabab=cabababaabac.

Reduce LHS:

Reduce RHS:

Defines rule #17.

Referenced by [26], [27].

Overlap of [15] caabacab=cbaac with [1] ababaab=abba:

Critical pair: caabacabba=cbaacabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #26.

Overlap of [15] caabacab=cbaac with [5] ababac=cab:

Critical pair: caabaccab=cbaacabac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [7] abbaabac=cabab with [16] cbaacab=cabbaac:

Critical pair: abbaabacabbaac=cababbaacab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [16] cbaacab=cabbaac with [1] ababaab=abba:

Critical pair: cbaacabba=cabbaacabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [16] cbaacab=cabbaac with [5] ababac=cab:

Critical pair: cbaaccab=cabbaacabac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #25.