Certificate for #3345 ⟨a, b | aaaaababaa=a⟩

Completion settings:

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

Axiom: aaaaababaa=a.

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

Axiom: aaaaaa=c.

Defines rule #2.

Referenced by [3], [5], [6], [8], [9], [13], [18], [19], [20], [22], [23], [24], [25], [26].

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

Critical pair: ac=ca.

Defines rule #1.

Referenced by [18], [20], [22], [23], [24], [25], [26].

Overlap of [1] aaaaababaa=a with [1] aaaaababaa=a:

Critical pair: aaaaababa=aaaababaa.

Referenced by [7], [10], [13].

Overlap of [2] aaaaaa=c with [1] aaaaababaa=a:

Critical pair: aa=cbabaa.

Flip LHS and RHS.

Referenced by [7], [8], [9].

Overlap of [2] aaaaaa=c with [1] aaaaababaa=a:

Critical pair: aaa=cababaa.

Flip LHS and RHS.

Referenced by [9].

Overlap of [5] cbabaa=aa with [1] aaaaababaa=a:

Critical pair: cbaba=aaaaababaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [10], [11].

Overlap of [5] cbabaa=aa with [2] aaaaaa=c:

Critical pair: cbabc=aaaaaa.

Reduce RHS:

Referenced by [19].

Overlap of [6] cababaa=aaa with [1] aaaaababaa=a:

Critical pair: cababa=aaaaaababaa.

Reduce RHS:

Defines rule #14.

Referenced by [13], [17].

Overlap of [1] aaaaababaa=a with [4] aaaaababa=aaaababaa:

Critical pair: aaaababaaa=a.

Reduce LHS:

Defines rule #13.

Referenced by [11], [14], [16].

Simplify [7] aaaababaaa=cbaba.

Reduce RHS:

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

Overlap of [11] aaaababaaa=a with [11] aaaababaaa=a:

Critical pair: aaaababa=aababaaa.

Referenced by [13], [14], [15].

Overlap of [9] cababa=aa with [11] aaaababaaa=a:

Critical pair: cababa=aaaaababaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [15], [21].

Overlap of [10] cbaba=a with [11] aaaababaaa=a:

Critical pair: cbaba=aaaababaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [11] aaaababaaa=a with [13] aababc=aa:

Critical pair: aaaababaaa=ababc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [10] cbaba=a with [15] ababc=a:

Critical pair: cba=abc.

Flip LHS and RHS.

Defines rule #3.

Referenced by [18], [19], [20], [22], [23], [24], [25], [26].

Overlap of [15] ababc=a with [9] cababa=aa:

Critical pair: ababaa=aababa.

Flip LHS and RHS.

Defines rule #15.

Overlap of [2] aaaaaa=c with [16] abc=cba:

Critical pair: aaaaacba=cbc.

Reduce LHS:

Defines rule #10.

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

Overlap of [16] abc=cba with [18] caaaaaba=cbc:

Critical pair: abcbc=cbaaaaaaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [18] caaaaaba=cbc with [2] aaaaaa=c:

Critical pair: caaaaabc=cbcaaaaa.

Reduce LHS:

Defines rule #9.

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

Overlap of [18] caaaaaba=cbc with [13] aababc=aa:

Critical pair: caaaaa=cbcbc.

Flip LHS and RHS.

Defines rule #11.

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

Overlap of [20] ccaaaaba=cbcaaaaa with [2] aaaaaa=c:

Critical pair: ccaaaabc=cbcaaaaaaaaaa.

Reduce LHS:

Reduce RHS:

Defines rule #8.

Referenced by [23].

Overlap of [21] cbcbc=caaaaa with [22] cccaaaba=cbccaaaa:

Critical pair: cbcbcbccaaaa=caaaaaccaaaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [24].

Overlap of [21] cbcbc=caaaaa with [23] ccccaaba=cbcccaaa:

Critical pair: cbcbcbcccaaa=caaaaacccaaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [25].

Overlap of [21] cbcbc=caaaaa with [24] cccccaba=cbccccaa:

Critical pair: cbcbcbccccaa=caaaaaccccaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [26].

Overlap of [21] cbcbc=caaaaa with [25] ccccccba=cbccccca:

Critical pair: cbcbcbccccca=caaaaacccccba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.