Certificate for #3501 ⟨a, b | aaabbabbaa=a⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with b < a < c
• Auxiliary generators:
  1. abba=c

Axiom: aaabbabbaa=a.

Referenced by [3].

Axiom: abba=c.

Defines rule #1.

Referenced by [3], [4], [6], [7], [14], [15], [17], [19].

Overlap of [1] aaabbabbaa=a with [2] abba=c:

Critical pair: aacbbaa=a.

Referenced by [5].

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

Critical pair: abbc=cbba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [17].

Simplify [3] aacbbaa=a.

Reduce LHS:

Referenced by [6], [7], [8], [10].

Overlap of [2] abba=c with [5] aaabbca=a:

Critical pair: abba=caabbca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9], [12], [18].

Overlap of [5] aaabbca=a with [2] abba=c:

Critical pair: aaabbcc=abba.

Reduce RHS:

Referenced by [11].

Overlap of [5] aaabbca=a with [6] caabbca=c:

Critical pair: aaabbc=aabbca.

Referenced by [10], [11].

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

Critical pair: caabbc=cabbca.

Referenced by [18].

Overlap of [5] aaabbca=a with [8] aaabbc=aabbca:

Critical pair: aabbcaa=a.

Referenced by [12], [16].

Overlap of [7] aaabbcc=c with [8] aaabbc=aabbca:

Critical pair: aabbcac=c.

Referenced by [13].

Overlap of [10] aabbcaa=a with [6] caabbca=c:

Critical pair: aabbc=abbca.

Defines rule #5.

Referenced by [13], [15], [16], [17], [21], [22].

Simplify [11] aabbcac=c.

Reduce LHS:

Referenced by [14], [22].

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

Critical pair: abbc=cbbcaac.

Flip LHS and RHS.

Referenced by [23].

Overlap of [2] abba=c with [12] aabbc=abbca:

Critical pair: abbabbca=cabbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [18], [23].

Overlap of [10] aabbcaa=a with [12] aabbc=abbca:

Critical pair: abbcaaa=a.

Referenced by [23].

Overlap of [12] aabbc=abbca with [4] cbba=abbc:

Critical pair: aabbabbc=abbcabba.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Referenced by [19], [20].

Overlap of [6] caabbca=c with [9] caabbc=cabbca:

Critical pair: cabbcaa=c.

Reduce LHS:

Referenced by [20].

Overlap of [2] abba=c with [17] acbbc=abbcc:

Critical pair: abbabbcc=ccbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [17] acbbc=abbcc with [18] cbbcaaa=c:

Critical pair: ac=abbccaaa.

Flip LHS and RHS.

Referenced by [21].

Overlap of [12] aabbc=abbca with [20] abbccaaa=ac:

Critical pair: aac=abbcacaaa.

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [12] aabbc=abbca with [21] abbcacaaa=aac:

Critical pair: aaac=abbcaacaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [15] cabbc=cbbca with [21] abbcacaaa=aac:

Critical pair: caac=cbbcaacaaa.

Reduce RHS:

Defines rule #4.