Certificate for #4594 ⟨a, b | abba=b, aaaaa=1⟩

Completion settings:

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

Axiom: abba=b.

Defines rule #4.

Referenced by [3], [4], [5], [6], [7], [8], [14], [15], [16], [18], [19], [21].

Axiom: aaaaa=1.

Defines rule #11.

Referenced by [4], [5].

Overlap of [1] abba=b with [1] abba=b:

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [10], [11], [12], [13], [16], [18], [19], [21], [22].

Overlap of [1] abba=b with [2] aaaaa=1:

Critical pair: abb=baaaa.

Flip LHS and RHS.

Referenced by [7].

Overlap of [2] aaaaa=1 with [1] abba=b:

Critical pair: aaaab=bba.

Referenced by [6].

Overlap of [5] aaaab=bba with [1] abba=b:

Critical pair: aaab=bbaba.

Defines rule #6.

Referenced by [9].

Overlap of [1] abba=b with [4] baaaa=abb:

Critical pair: ababb=baaa.

Flip LHS and RHS.

Defines rule #8.

Referenced by [8], [10], [16].

Overlap of [1] abba=b with [7] baaa=ababb:

Critical pair: abababb=baa.

Referenced by [9], [10], [11], [13], [16], [20], [23].

Overlap of [6] aaab=bbaba with [8] abababb=baa:

Critical pair: aabaa=bbabaababb.

Flip LHS and RHS.

Referenced by [17].

Overlap of [7] baaa=ababb with [8] abababb=baa:

Critical pair: baabaa=ababbbababb.

Reduce RHS:

Defines rule #9.

Referenced by [16].

Overlap of [8] abababb=baa with [3] bbba=abbb:

Critical pair: ababaabbb=baaba.

Referenced by [12], [16].

Overlap of [11] ababaabbb=baaba with [3] bbba=abbb:

Critical pair: ababaababbb=baababa.

Referenced by [13].

Overlap of [12] ababaababbb=baababa with [3] bbba=abbb:

Critical pair: ababaabababbb=baabababa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [14], [15].

Overlap of [1] abba=b with [13] baabababa=abababaab:

Critical pair: ababababaab=babababa.

Referenced by [15], [16].

Overlap of [13] baabababa=abababaab with [14] ababababaab=babababa:

Critical pair: bababababa=abababaabbaab.

Reduce RHS:

Referenced by [16].

Overlap of [14] ababababaab=babababa with [11] ababaabbb=baaba:

Critical pair: abababababaaba=babababaabaabbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [17], [18].

Overlap of [9] bbabaababb=aabaa with [16] aababbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=aaba:

Critical pair: bbabaaba=aabaabbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Defines rule #10.

Overlap of [16] aababbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=aaba with [3] bbba=abbb:

Critical pair: aababbbbbbbbbbbbbbbbbbbbbbbbbbbbbabbb=aababba.

Reduce LHS:

Reduce RHS:

Referenced by [19].

Overlap of [18] aabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=aabb with [3] bbba=abbb:

Critical pair: aabbbbbbbbbbbbbbbbbbbbbbbbbbbbbabbb=aabba.

Reduce LHS:

Reduce RHS:

Referenced by [20], [21].

Overlap of [8] abababb=baa with [19] abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=ab:

Critical pair: ababab=baabbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Referenced by [23], [24].

Overlap of [19] abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=ab with [3] bbba=abbb:

Critical pair: abbbbbbbbbbbbbbbbbbbbbbbbbbbbbabbb=abba.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [22].

Overlap of [21] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=b with [3] bbba=abbb:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbabbb=ba.

Reduce LHS:

Defines rule #2.

Referenced by [24].

Overlap of [8] abababb=baa with [20] ababab=baabbbbbbbbbbbbbbbbbbbbbbbbbbbbb:

Critical pair: baabbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=baa.

Defines rule #5.

Referenced by [24].

Overlap of [20] ababab=baabbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [22] babbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=ba:

Critical pair: ababa=baabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.

Reduce RHS:

Defines rule #7.