Certificate for #4824 ⟨a, b | abababba=aab⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with a < b

Axiom: abababba=aab.

Defines rule #1.

Referenced by [2], [3], [4], [5], [7], [8], [9].

Overlap of [1] abababba=aab with [1] abababba=aab:

Critical pair: abababbaab=aabbababba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4], [6].

Overlap of [1] abababba=aab with [2] aabbababba=aabab:

Critical pair: abababbaabab=aababbababba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [10].

Overlap of [2] aabbababba=aabab with [2] aabbababba=aabab:

Critical pair: aabbababbaabab=aabababbababba.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [5], [6], [7], [8], [9], [10].

Overlap of [1] abababba=aab with [4] aabababab=aaabbabba:

Critical pair: abababbaaabbabba=aababababab.

Reduce LHS:

Reduce RHS:

Defines rule #5.

Overlap of [2] aabbababba=aabab with [4] aabababab=aaabbabba:

Critical pair: aabbababbaaabbabba=aabababababab.

Reduce LHS:

Reduce RHS:

Defines rule #8.

Overlap of [4] aabababab=aaabbabba with [1] abababba=aab:

Critical pair: aabaab=aaabbabbaba.

Flip LHS and RHS.

Defines rule #4.

Overlap of [4] aabababab=aaabbabba with [1] abababba=aab:

Critical pair: aababaab=aaabbabbaabba.

Flip LHS and RHS.

Defines rule #7.

Overlap of [4] aabababab=aaabbabba with [1] abababba=aab:

Critical pair: aabababaab=aaabbabbaababba.

Flip LHS and RHS.

Defines rule #9.

Overlap of [3] aababbababba=aababab with [4] aabababab=aaabbabba:

Critical pair: aababbababbaaabbabba=aababababababab.

Reduce LHS:

Reduce RHS:

Defines rule #10.