Certificate for #22800 ⟨a, b | aaa=1, ababb=bba⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(b) = 0; deg(a) = 1

Axiom: aaa=1.

Defines rule #2.

Referenced by [3], [4].

Axiom: ababb=bba.

Defines rule #1.

Referenced by [3], [5], [7].

Overlap of [1] aaa=1 with [2] ababb=bba:

Critical pair: aabba=babb.

Defines rule #4.

Referenced by [4], [5], [6], [7], [8], [10], [14].

Overlap of [3] aabba=babb with [1] aaa=1:

Critical pair: aabb=babbaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7], [8], [9], [11], [15], [18].

Overlap of [3] aabba=babb with [2] ababb=bba:

Critical pair: aabbbba=babbbabb.

Defines rule #5.

Referenced by [9], [10], [11], [12], [13], [16].

Overlap of [3] aabba=babb with [3] aabba=babb:

Critical pair: aabbbabb=babbabba.

Defines rule #6.

Referenced by [16].

Overlap of [2] ababb=bba with [4] babbaa=aabb:

Critical pair: ababaabb=bbaabbaa.

Reduce RHS:

Defines rule #10.

Referenced by [14], [15].

Overlap of [3] aabba=babb with [4] babbaa=aabb:

Critical pair: aabaabb=babbbbaa.

Defines rule #9.

Referenced by [13].

Overlap of [4] babbaa=aabb with [5] aabbbba=babbbabb:

Critical pair: babbbabbbabb=aabbbbbba.

Defines rule #7.

Overlap of [5] aabbbba=babbbabb with [3] aabba=babb:

Critical pair: aabbbbbabb=babbbabbabba.

Flip LHS and RHS.

Defines rule #8.

Overlap of [5] aabbbba=babbbabb with [4] babbaa=aabb:

Critical pair: aabbbaabb=babbbabbbbaa.

Defines rule #12.

Referenced by [17].

Overlap of [5] aabbbba=babbbabb with [5] aabbbba=babbbabb:

Critical pair: aabbbbbabbbabb=babbbabbabbbba.

Defines rule #13.

Overlap of [5] aabbbba=babbbabb with [8] aabaabb=babbbbaa:

Critical pair: aabbbbbabbbbaa=babbbabbabaabb.

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] aabba=babb with [7] ababaabb=bbbabba:

Critical pair: aabbbbbabba=babbbabaabb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [17].

Overlap of [4] babbaa=aabb with [7] ababaabb=bbbabba:

Critical pair: babbabbbabba=aabbbabaabb.

Flip LHS and RHS.

Defines rule #16.

Referenced by [18].

Overlap of [5] aabbbba=babbbabb with [6] aabbbabb=babbabba:

Critical pair: aabbbbbabbabba=babbbabbabbbabb.

Defines rule #14.

Overlap of [14] babbbabaabb=aabbbbbabba with [11] aabbbaabb=babbbabbbbaa:

Critical pair: babbbabbabbbabbbbaa=aabbbbbabbabaabb.

Flip LHS and RHS.

Defines rule #18.

Overlap of [4] babbaa=aabb with [15] aabbbabaabb=babbabbbabba:

Critical pair: babbbabbabbbabba=aabbbbbabaabb.

Flip LHS and RHS.

Defines rule #17.