Certificate for #5211 ⟨a, b | aabbaab=abaa⟩

Completion settings:

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

Axiom: aabbaab=abaa.

Referenced by [3].

Axiom: abba=c.

Defines rule #2.

Referenced by [3], [4], [5], [6], [7], [8], [9], [10], [14].

Overlap of [1] aabbaab=abaa with [2] abba=c:

Critical pair: acab=abaa.

Flip LHS and RHS.

Defines rule #8.

Referenced by [5], [6], [7], [9], [11], [12], [15], [16], [18], [20], [21].

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

Critical pair: abbc=cbba.

Flip LHS and RHS.

Defines rule #1.

Overlap of [2] abba=c with [3] abaa=acab:

Critical pair: abbacab=cbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [8], [9], [13], [17].

Overlap of [3] abaa=acab with [2] abba=c:

Critical pair: abac=acabbba.

Flip LHS and RHS.

Defines rule #10.

Overlap of [3] abaa=acab with [3] abaa=acab:

Critical pair: abaacab=acabbaa.

Reduce LHS:

Reduce RHS:

Defines rule #9.

Referenced by [12], [13], [14], [15], [16], [19], [20].

Overlap of [5] cbaa=ccab with [2] abba=c:

Critical pair: cbac=ccabbba.

Flip LHS and RHS.

Defines rule #5.

Overlap of [5] cbaa=ccab with [3] abaa=acab:

Critical pair: cbaacab=ccabbaa.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [10], [11], [13], [17].

Overlap of [9] ccabcab=ccca with [2] abba=c:

Critical pair: ccabcc=cccaba.

Flip LHS and RHS.

Defines rule #6.

Overlap of [9] ccabcab=ccca with [3] abaa=acab:

Critical pair: ccabcacab=cccaaa.

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] abaa=acab with [7] acabcab=acca:

Critical pair: abaacca=acabcabcab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [20], [21].

Overlap of [5] cbaa=ccab with [7] acabcab=acca:

Critical pair: cbaacca=ccabcabcab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [18], [19].

Overlap of [7] acabcab=acca with [2] abba=c:

Critical pair: acabcc=accaba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [16], [17].

Overlap of [7] acabcab=acca with [3] abaa=acab:

Critical pair: acabcacab=accaaa.

Flip LHS and RHS.

Defines rule #18.

Overlap of [3] abaa=acab with [14] accaba=acabcc:

Critical pair: abaacabcc=acabccaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [5] cbaa=ccab with [14] accaba=acabcc:

Critical pair: cbaacabcc=ccabccaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [13] cccacab=ccabcca with [3] abaa=acab:

Critical pair: cccacacab=ccabccaaa.

Flip LHS and RHS.

Defines rule #19.

Overlap of [13] cccacab=ccabcca with [7] acabcab=acca:

Critical pair: cccacca=ccabccacab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [3] abaa=acab with [12] accacab=acabcca:

Critical pair: abaacabcca=acabccacab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [12] accacab=acabcca with [3] abaa=acab:

Critical pair: accacacab=acabccaaa.

Flip LHS and RHS.

Defines rule #20.