Certificate for #4023 ⟨a, b | aaabbabaa=ab⟩

Completion settings:

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

Axiom: aaabbabaa=ab.

Referenced by [3].

Axiom: abb=c.

Defines rule #4.

Referenced by [3], [4], [6], [9], [21], [24], [25].

Overlap of [1] aaabbabaa=ab with [2] abb=c:

Critical pair: aacabaa=ab.

Defines rule #1.

Referenced by [4], [5], [6], [7], [8], [9], [11], [15], [18], [25].

Overlap of [3] aacabaa=ab with [2] abb=c:

Critical pair: aacabac=abbb.

Reduce RHS:

Defines rule #2.

Referenced by [7], [8], [9], [10], [12], [13], [16], [17], [19], [20], [26].

Overlap of [3] aacabaa=ab with [3] aacabaa=ab:

Critical pair: aacabab=abcabaa.

Defines rule #10.

Referenced by [21], [22].

Overlap of [3] aacabaa=ab with [3] aacabaa=ab:

Critical pair: aacabaab=abacabaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [3] aacabaa=ab with [4] aacabac=cb:

Critical pair: aacabcb=abcabac.

Defines rule #11.

Referenced by [23].

Overlap of [3] aacabaa=ab with [4] aacabac=cb:

Critical pair: aacabacb=abacabac.

Reduce LHS:

Defines rule #6.

Referenced by [22], [23].

Overlap of [3] aacabaa=ab with [6] abacabaa=c:

Critical pair: aacabac=abbacabaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [15], [16], [17], [22], [23].

Overlap of [4] aacabac=cb with [6] abacabaa=c:

Critical pair: aacc=cbabaa.

Flip LHS and RHS.

Defines rule #7.

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

Overlap of [6] abacabaa=c with [3] aacabaa=ab:

Critical pair: abacabab=ccabaa.

Defines rule #16.

Overlap of [6] abacabaa=c with [4] aacabac=cb:

Critical pair: abacabcb=ccabac.

Defines rule #17.

Overlap of [6] abacabaa=c with [4] aacabac=cb:

Critical pair: abacabacb=cacabac.

Defines rule #18.

Overlap of [6] abacabaa=c with [6] abacabaa=c:

Critical pair: abacabac=cbacabaa.

Flip LHS and RHS.

Defines rule #8.

Referenced by [26].

Overlap of [9] cacabaa=cb with [3] aacabaa=ab:

Critical pair: cacabab=cbcabaa.

Defines rule #12.

Referenced by [24].

Overlap of [9] cacabaa=cb with [4] aacabac=cb:

Critical pair: cacabcb=cbcabac.

Defines rule #13.

Overlap of [9] cacabaa=cb with [4] aacabac=cb:

Critical pair: cacabacb=cbacabac.

Defines rule #14.

Overlap of [10] cbabaa=aacc with [3] aacabaa=ab:

Critical pair: cbabab=aacccabaa.

Defines rule #19.

Overlap of [10] cbabaa=aacc with [4] aacabac=cb:

Critical pair: cbabcb=aacccabac.

Defines rule #20.

Overlap of [10] cbabaa=aacc with [4] aacabac=cb:

Critical pair: cbabacb=aaccacabac.

Defines rule #21.

Overlap of [5] aacabab=abcabaa with [2] abb=c:

Critical pair: aacabc=abcabaab.

Flip LHS and RHS.

Defines rule #15.

Referenced by [25].

Overlap of [9] cacabaa=cb with [5] aacabab=abcabaa:

Critical pair: cacabaabcabaa=cbacabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [9] cacabaa=cb with [7] aacabcb=abcabac:

Critical pair: cacabaabcabac=cbacabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [15] cacabab=cbcabaa with [2] abb=c:

Critical pair: cacabc=cbcabaab.

Flip LHS and RHS.

Defines rule #22.

Overlap of [3] aacabaa=ab with [21] abcabaab=aacabc:

Critical pair: aacabaaacabc=abbcabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [14] cbacabaa=abacabac with [4] aacabac=cb:

Critical pair: cbacabacb=abacabacacabac.

Defines rule #25.