Certificate for #5728 ⟨a, b | aaaa=1, babbb=a⟩

Completion settings:

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

Axiom: aaaa=1.

Defines rule #3.

Referenced by [4], [5], [10], [14], [16], [18], [19], [21], [24], [25], [28].

Axiom: babbb=a.

Referenced by [3], [6], [7], [8], [11], [12], [13], [16], [17], [18], [19], [20], [21], [23], [26], [27].

Overlap of [2] babbb=a with [2] babbb=a:

Critical pair: babba=aabbb.

Flip LHS and RHS.

Referenced by [4], [9], [13], [18], [19].

Overlap of [1] aaaa=1 with [3] aabbb=babba:

Critical pair: aababba=bbb.

Referenced by [5], [6], [9].

Overlap of [4] aababba=bbb with [1] aaaa=1:

Critical pair: aababb=bbbaaa.

Referenced by [7], [9], [12].

Overlap of [4] aababba=bbb with [2] babbb=a:

Critical pair: aababa=bbbbbb.

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

Overlap of [5] aababb=bbbaaa with [2] babbb=a:

Critical pair: aaa=bbbaaab.

Flip LHS and RHS.

Referenced by [8], [9], [14], [16], [18], [19].

Overlap of [2] babbb=a with [7] bbbaaab=aaa:

Critical pair: babaaa=abaaab.

Flip LHS and RHS.

Referenced by [14].

Overlap of [4] aababba=bbb with [6] aababa=bbbbbb:

Critical pair: aababbbbbbbb=bbbababa.

Reduce LHS:

Referenced by [15].

Overlap of [6] aababa=bbbbbb with [1] aaaa=1:

Critical pair: aabab=bbbbbbaaa.

Referenced by [14].

Overlap of [6] aababa=bbbbbb with [2] babbb=a:

Critical pair: aabaa=bbbbbbbbb.

Referenced by [12].

Overlap of [6] aababa=bbbbbb with [5] aababb=bbbaaa:

Critical pair: aababbbbaaa=bbbbbbababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [6] aababa=bbbbbb with [6] aababa=bbbbbb:

Critical pair: aababbbbbbb=bbbbbbababa.

Reduce LHS:

Referenced by [15], [19].

Overlap of [7] bbbaaab=aaa with [8] abaaab=babaaa:

Critical pair: bbbaababaaa=aaaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [18], [19], [21], [23].

Simplify [9] ababbabb=bbbababa.

Reduce LHS:

Referenced by [16], [17], [18], [19].

Overlap of [2] babbb=a with [15] bbbbbbababab=bbbababa:

Critical pair: babbbababa=abbbababab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [2] babbb=a with [15] bbbbbbababab=bbbababa:

Critical pair: babbbbababa=abbbbababab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20], [22], [23].

Overlap of [3] aabbb=babba with [15] bbbbbbababab=bbbababa:

Critical pair: aabbbababa=babbabbbababab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19], [23], [26].

Overlap of [3] aabbb=babba with [15] bbbbbbababab=bbbababa:

Critical pair: aabbbbbababa=babbabbbbbababab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [2] babbb=a with [17] abbbbababab=abababa:

Critical pair: babababa=abababab.

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [14] aab=bbbbbbbbbaa with [20] abababab=babababa:

Critical pair: ababababa=bbbbbbbbbaaababab.

Reduce LHS:

Reduce RHS:

Referenced by [25].

Overlap of [16] abbbababab=bbbbbb with [20] abababab=babababa:

Critical pair: abbbbabababa=bbbbbbab.

Reduce LHS:

Referenced by [23], [24].

Overlap of [17] abbbbababab=abababa with [22] abababaa=bbbbbbab:

Critical pair: abbbbbbbbbbab=abababaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [22] abababaa=bbbbbbab with [1] aaaa=1:

Critical pair: ababab=bbbbbbabaa.

Reduce RHS:

Referenced by [25].

Simplify [21] babababaa=bbbbbbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27], [29].

Overlap of [2] babbb=a with [18] abbbbb=bbbbbbbbbbbbbbbbbbbbbbbbba:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbba=abb.

Flip LHS and RHS.

Referenced by [27].

Overlap of [2] babbb=a with [26] abb=bbbbbbbbbbbbbbbbbbbbbbbbbba:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbab=a.

Reduce LHS:

Referenced by [28], [29].

Overlap of [27] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=a with [1] aaaa=1:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=aaaa.

Reduce RHS:

Defines rule #1.

Referenced by [29].

Overlap of [27] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=a with [25] bbbbbbbab=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba:

Critical pair: bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=ab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.