Certificate for #4140 ⟨a, b | aababbbaa=ab⟩

Completion settings:

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

Axiom: aababbbaa=ab.

Referenced by [3].

Axiom: abbba=c.

Defines rule #13.

Referenced by [3], [4], [5], [6], [14], [22], [42], [49].

Overlap of [1] aababbbaa=ab with [2] abbba=c:

Critical pair: aabca=ab.

Defines rule #1.

Referenced by [5], [6], [7], [8], [9], [11], [17], [35], [36], [38].

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

Critical pair: abbbc=cbbba.

Flip LHS and RHS.

Defines rule #18.

Referenced by [16], [20], [21], [26], [28], [30], [32].

Overlap of [2] abbba=c with [3] aabca=ab:

Critical pair: abbbab=cabca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [8], [9], [10], [12], [13], [15], [39], [46].

Overlap of [3] aabca=ab with [2] abbba=c:

Critical pair: aabcc=abbbba.

Flip LHS and RHS.

Referenced by [23].

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

Critical pair: aabcab=ababca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [12], [13], [14], [16], [18], [40], [43], [44], [45], [47].

Overlap of [3] aabca=ab with [5] cabca=cb:

Critical pair: aabcb=abbca.

Defines rule #6.

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

Overlap of [5] cabca=cb with [3] aabca=ab:

Critical pair: cabcab=cbabca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [15], [16], [19], [34], [37], [41], [48].

Overlap of [5] cabca=cb with [5] cabca=cb:

Critical pair: cabcb=cbbca.

Defines rule #12.

Referenced by [21], [25].

Overlap of [3] aabca=ab with [7] ababca=abb:

Critical pair: aabcabb=abbabca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [22], [42], [49].

Overlap of [5] cabca=cb with [7] ababca=abb:

Critical pair: cabcabb=cbbabca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [7] ababca=abb with [5] cabca=cb:

Critical pair: ababcb=abbbca.

Defines rule #16.

Referenced by [26], [27].

Overlap of [7] ababca=abb with [7] ababca=abb:

Critical pair: ababcabb=abbbabca.

Reduce LHS:

Reduce RHS:

Defines rule #24.

Referenced by [17], [18], [22], [23], [40], [42], [47], [49].

Overlap of [9] cbabca=cbb with [5] cabca=cb:

Critical pair: cbabcb=cbbbca.

Defines rule #22.

Referenced by [28], [29].

Overlap of [9] cbabca=cbb with [7] ababca=abb:

Critical pair: cbabcabb=cbbbabca.

Reduce LHS:

Reduce RHS:

Defines rule #30.

Referenced by [19], [34], [37], [41], [48].

Overlap of [3] aabca=ab with [14] abbbb=cbca:

Critical pair: aabccbca=abbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [22], [42], [49].

Overlap of [7] ababca=abb with [8] aabcb=abbca:

Critical pair: ababcabbca=abbabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Referenced by [30], [31].

Overlap of [9] cbabca=cbb with [8] aabcb=abbca:

Critical pair: cbabcabbca=cbbabcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Overlap of [8] aabcb=abbca with [4] cbbba=abbbc:

Critical pair: aababbbc=abbcabba.

Defines rule #28.

Referenced by [37].

Overlap of [10] cabcb=cbbca with [4] cbbba=abbbc:

Critical pair: cababbbc=cbbcabba.

Defines rule #36.

Overlap of [11] abbabca=abbb with [8] aabcb=abbca:

Critical pair: abbabcabbca=abbbabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [32], [33].

Overlap of [6] abbbba=aabcc with [14] abbbb=cbca:

Critical pair: cbcaa=aabcc.

Defines rule #2.

Referenced by [24], [25], [27], [29], [31], [33], [35], [36], [38], [43], [44], [45].

Overlap of [8] aabcb=abbca with [23] cbcaa=aabcc:

Critical pair: aabaabcc=abbcacaa.

Defines rule #5.

Referenced by [34], [35].

Overlap of [10] cabcb=cbbca with [23] cbcaa=aabcc:

Critical pair: cabaabcc=cbbcacaa.

Defines rule #11.

Referenced by [36].

Overlap of [13] ababcb=abbbca with [4] cbbba=abbbc:

Critical pair: abababbbc=abbbcabba.

Defines rule #39.

Overlap of [13] ababcb=abbbca with [23] cbcaa=aabcc:

Critical pair: ababaabcc=abbbcacaa.

Defines rule #15.

Referenced by [38].

Overlap of [15] cbabcb=cbbbca with [4] cbbba=abbbc:

Critical pair: cbababbbc=cbbbcabba.

Defines rule #42.

Overlap of [15] cbabcb=cbbbca with [23] cbcaa=aabcc:

Critical pair: cbabaabcc=cbbbcacaa.

Defines rule #21.

Overlap of [18] abbabcb=cbcaca with [4] cbbba=abbbc:

Critical pair: abbababbbc=cbcacabba.

Defines rule #44.

Overlap of [18] abbabcb=cbcaca with [23] cbcaa=aabcc:

Critical pair: abbabaabcc=cbcacacaa.

Defines rule #25.

Overlap of [22] cbcb=aabccbcaca with [4] cbbba=abbbc:

Critical pair: cbabbbc=aabccbcacabba.

Defines rule #33.

Overlap of [22] cbcb=aabccbcaca with [23] cbcaa=aabcc:

Critical pair: cbaabcc=aabccbcacacaa.

Defines rule #8.

Overlap of [9] cbabca=cbb with [24] aabaabcc=abbcacaa:

Critical pair: cbabcabbcacaa=cbbabaabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [24] aabaabcc=abbcacaa with [23] cbcaa=aabcc:

Critical pair: aabaabcaabcc=abbcacaabcaa.

Reduce LHS:

Reduce RHS:

Defines rule #17.

Referenced by [39], [40], [41], [42], [43].

Overlap of [25] cabaabcc=cbbcacaa with [23] cbcaa=aabcc:

Critical pair: cabaabcaabcc=cbbcacaabcaa.

Reduce LHS:

Reduce RHS:

Defines rule #23.

Referenced by [44].

Overlap of [9] cbabca=cbb with [20] aababbbc=abbcabba:

Critical pair: cbabcabbcabba=cbbababbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #46.

Overlap of [27] ababaabcc=abbbcacaa with [23] cbcaa=aabcc:

Critical pair: ababaabcaabcc=abbbcacaabcaa.

Reduce LHS:

Reduce RHS:

Defines rule #27.

Referenced by [45].

Overlap of [5] cabca=cb with [35] aabababcc=abbcacaba:

Critical pair: cabcabbcacaba=cbabababcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #35.

Overlap of [7] ababca=abb with [35] aabababcc=abbcacaba:

Critical pair: ababcabbcacaba=abbabababcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #38.

Overlap of [9] cbabca=cbb with [35] aabababcc=abbcacaba:

Critical pair: cbabcabbcacaba=cbbabababcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Overlap of [11] abbabca=abbb with [35] aabababcc=abbcacaba:

Critical pair: abbabcabbcacaba=abbbabababcc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [35] aabababcc=abbcacaba with [23] cbcaa=aabcc:

Critical pair: aabababcaabcc=abbcacababcaa.

Reduce LHS:

Reduce RHS:

Defines rule #29.

Referenced by [46], [47], [48], [49].

Overlap of [36] cabababcc=cbbcacaba with [23] cbcaa=aabcc:

Critical pair: cabababcaabcc=cbbcacababcaa.

Reduce LHS:

Reduce RHS:

Defines rule #37.

Overlap of [38] ababababcc=abbbcacaba with [23] cbcaa=aabcc:

Critical pair: ababababcaabcc=abbbcacababcaa.

Reduce LHS:

Reduce RHS:

Defines rule #40.

Overlap of [5] cabca=cb with [43] aababbabcc=abbcacabba:

Critical pair: cabcabbcacabba=cbababbabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #43.

Overlap of [7] ababca=abb with [43] aababbabcc=abbcacabba:

Critical pair: ababcabbcacabba=abbababbabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #45.

Overlap of [9] cbabca=cbb with [43] aababbabcc=abbcacabba:

Critical pair: cbabcabbcacabba=cbbababbabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #47.

Overlap of [11] abbabca=abbb with [43] aababbabcc=abbcacabba:

Critical pair: abbabcabbcacabba=abbbababbabcc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #34.