Certificate for #4591 ⟨a, b | aabaaaab=aba⟩

Completion settings:

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

Axiom: aabaaaab=aba.

Referenced by [3].

Axiom: aaaab=c.

Defines rule #13.

Referenced by [3], [4], [5], [10], [11], [12], [13], [14], [16], [18].

Overlap of [1] aabaaaab=aba with [2] aaaab=c:

Critical pair: aabc=aba.

Flip LHS and RHS.

Defines rule #10.

Referenced by [4], [5], [6], [7], [8], [11], [12], [14], [18].

Overlap of [2] aaaab=c with [3] aba=aabc:

Critical pair: aaaaabc=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [5], [6], [7], [8], [9], [11], [12], [13], [14], [18].

Overlap of [3] aba=aabc with [2] aaaab=c:

Critical pair: abc=aabcaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [13], [14], [15], [17], [18].

Overlap of [3] aba=aabc with [3] aba=aabc:

Critical pair: abaabc=aabcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [10], [11], [12], [13], [15], [18].

Overlap of [4] ca=acc with [3] aba=aabc:

Critical pair: caabc=accba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9].

Overlap of [3] aba=aabc with [7] accba=aaccccbc:

Critical pair: abaaccccbc=aabcccba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12], [13].

Overlap of [4] ca=acc with [7] accba=aaccccbc:

Critical pair: caaccccbc=accccba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaaab=c with [6] aabcba=aaabcccbc:

Critical pair: aaaaabcccbc=ccba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

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

Overlap of [3] aba=aabc with [6] aabcba=aaabcccbc:

Critical pair: abaaabcccbc=aabcabcba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [16], [17].

Overlap of [6] aabcba=aaabcccbc with [2] aaaab=c:

Critical pair: aabcbc=aaabcccbcaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [18].

Overlap of [6] aabcba=aaabcccbc with [6] aabcba=aaabcccbc:

Critical pair: aabcbaaabcccbc=aaabcccbcabcba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [10] ccba=accccbc with [2] aaaab=c:

Critical pair: ccbc=accccbcaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [6] aabcba=aaabcccbc with [5] accccccccccccccccb=abc:

Critical pair: aabcbabc=aaabcccbcccccccccccccccccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [2] aaaab=c with [11] aaabcccbcba=ccccccccbcccbc:

Critical pair: accccccccbcccbc=ccccbcba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [18].

Overlap of [11] aaabcccbcba=ccccccccbcccbc with [5] accccccccccccccccb=abc:

Critical pair: aaabcccbcbabc=ccccccccbcccbcccccccccccccccccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [16] ccccbcba=accccccccbcccbc with [2] aaaab=c:

Critical pair: ccccbcbc=accccccccbcccbcaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.