Certificate for #3623 ⟨a, b | aabbaaaaab=a⟩

Completion settings:

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

Axiom: aabbaaaaab=a.

Referenced by [3].

Axiom: aaaaa=c.

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

Overlap of [1] aabbaaaaab=a with [2] aaaaa=c:

Critical pair: aabbcb=a.

Referenced by [5], [6], [7], [10], [14], [16], [19], [25].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Referenced by [6], [7], [16], [17], [21], [22], [26], [27].

Overlap of [2] aaaaa=c with [3] aabbcb=a:

Critical pair: aaaa=cbbcb.

Referenced by [6], [8], [9], [10], [11], [17], [18].

Overlap of [2] aaaaa=c with [3] aabbcb=a:

Critical pair: aaaaa=cabbcb.

Reduce LHS:

Reduce RHS:

Referenced by [9], [12].

Overlap of [4] ca=ac with [3] aabbcb=a:

Critical pair: ca=acabbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [8], [11].

Overlap of [2] aaaaa=c with [7] aacbbcb=ac:

Critical pair: aaaac=ccbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [2] aaaaa=c with [5] aaaa=cbbcb:

Critical pair: cbbcba=c.

Reduce LHS:

Referenced by [12], [13], [15], [17], [20], [21].

Overlap of [5] aaaa=cbbcb with [3] aabbcb=a:

Critical pair: aaa=cbbcbbbcb.

Referenced by [11], [17], [18], [19], [20], [21].

Overlap of [5] aaaa=cbbcb with [7] aacbbcb=ac:

Critical pair: aaac=cbbcbcbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [24], [26].

Simplify [6] cbbcba=acbbcb.

Reduce RHS:

Referenced by [13], [24], [26], [28].

Overlap of [9] acbbcb=c with [12] cbbcba=c:

Critical pair: acbbc=cbcba.

Flip LHS and RHS.

Referenced by [14], [15], [16], [17], [21], [27].

Overlap of [3] aabbcb=a with [13] cbcba=acbbc:

Critical pair: aabbacbbc=acba.

Referenced by [23].

Overlap of [9] acbbcb=c with [13] cbcba=acbbc:

Critical pair: acbbacbbc=ccba.

Referenced by [16], [22], [29].

Overlap of [13] cbcba=acbbc with [3] aabbcb=a:

Critical pair: cbcba=acbbcabbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [13] cbcba=acbbc with [5] aaaa=cbbcb:

Critical pair: cbcbcbbcb=acbbcaaa.

Reduce RHS:

Defines rule #3.

Referenced by [21], [27], [37].

Overlap of [5] aaaa=cbbcb with [10] aaa=cbbcbbbcb:

Critical pair: cbbcbbbcba=cbbcb.

Referenced by [28].

Overlap of [10] aaa=cbbcbbbcb with [3] aabbcb=a:

Critical pair: aa=cbbcbbbcbbbcb.

Referenced by [20], [21], [22], [23], [25], [26], [27], [28].

Overlap of [10] aaa=cbbcbbbcb with [9] acbbcb=c:

Critical pair: aac=cbbcbbbcbcbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [24], [26], [28].

Overlap of [13] cbcba=acbbc with [10] aaa=cbbcbbbcb:

Critical pair: cbcbcbbcbbbcb=acbbcaa.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Referenced by [27], [38].

Overlap of [15] acbbacbbc=ccba with [4] ca=ac:

Critical pair: acbbacbbac=ccbaa.

Reduce RHS:

Referenced by [33].

Simplify [14] aabbacbbc=acba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [12] cbbcba=c with [23] acba=cbbcbbbcbbbcbbbacbbc:

Critical pair: cbbcbcbbcbbbcbbbcbbbacbbc=ccba.

Reduce LHS:

Referenced by [34].

Overlap of [3] aabbcb=a with [19] aa=cbbcbbbcbbbcb:

Critical pair: cbbcbbbcbbbcbbbcb=a.

Flip LHS and RHS.

Defines rule #14.

Referenced by [26], [27], [29], [30], [31], [32], [33], [34], [35].

Overlap of [12] cbbcba=c with [19] aa=cbbcbbbcbbbcb:

Critical pair: cbbcbcbbcbbbcbbbcb=ca.

Reduce LHS:

Reduce RHS:

Defines rule #10.

Referenced by [28], [35].

Overlap of [13] cbcba=acbbc with [19] aa=cbbcbbbcbbbcb:

Critical pair: cbcbcbbcbbbcbbbcb=acbbca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [18] cbbcbbbcba=cbbcb with [19] aa=cbbcbbbcbbbcb:

Critical pair: cbbcbbbcbcbbcbbbcbbbcb=cbbcba.

Reduce LHS:

Reduce RHS:

Defines rule #13.

Referenced by [30], [33], [35], [36], [37], [38].

Simplify [15] acbbacbbc=ccba.

Reduce RHS:

Referenced by [30].

Overlap of [29] acbbacbbc=ccbcbbcbbbcbbbcbbbcb with [25] a=cbbcbbbcbbbcbbbcb:

Critical pair: cbbcbbbcbbbcbbbcbcbbacbbc=ccbcbbcbbbcbbbcbbbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32].

Simplify [16] ccbab=acbbc.

Reduce RHS:

Referenced by [32].

Overlap of [31] ccbab=cbbcbbbcbbbcbbbcbcbbc with [25] a=cbbcbbbcbbbcbbbcb:

Critical pair: ccbcbbcbbbcbbbcbbbcbb=cbbcbbbcbbbcbbbcbcbbc.

Reduce LHS:

Defines rule #12.

Referenced by [33].

Overlap of [22] acbbacbbac=ccbcbbcbbbcbbbcb with [25] a=cbbcbbbcbbbcbbbcb:

Critical pair: cbbcbbbcbbbcbbbcbcbbacbbac=ccbcbbcbbbcbbbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34], [39].

Simplify [24] cbbcbbbcbbbcbcbbcbbbacbbc=ccba.

Reduce RHS:

Referenced by [35].

Overlap of [34] cbbcbbbcbbbcbcbbcbbbacbbc=ccbbbcbbbcbbbcbcbbcb with [26] cbbcbbbcbbbcbcbbcb=cbbcbbbcbbbcbbbcbc:

Critical pair: cbbcbbbcbbbcbbbcbcbbacbbc=ccbbbcbbbcbbbcbcbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [27] cbbcbbbcbbbcbbbcbcbbcbbcbbbcbbbcbbbcbc=cbcbbbcbbbcbcbbcb with [28] cbbcbbbcbbbcbbbcbcbbcb=c:

Critical pair: cbcbbbcbbbcbbbcbc=cbcbbbcbbbcbcbbcb.

Flip LHS and RHS.

Defines rule #9.

Overlap of [28] cbbcbbbcbbbcbbbcbcbbcb=c with [17] cbcbcbbcb=cbcbbbcbc:

Critical pair: cbbcbbbcbbbcbbbcbcbbcbcbbbcbc=ccbcbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [39].

Overlap of [28] cbbcbbbcbbbcbbbcbcbbcb=c with [21] cbcbbbcbcbbcb=cbcbbbcbbbcbc:

Critical pair: cbbcbbbcbbbcbbbcbcbbcbcbbbcbbbcbc=ccbbbcbcbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [39].

Overlap of [33] ccbcbbcbbbcbbbcb=ccbbbcbbbcbbbcbc with [37] ccbcbbcb=ccbbbcbc:

Critical pair: ccbbbcbcbbcbbbcb=ccbbbcbbbcbbbcbc.

Reduce LHS:

Defines rule #8.