Certificate for #3590 ⟨a, b | aabababaab=a⟩

Completion settings:

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

Axiom: aabababaab=a.

Referenced by [2], [3], [4], [6], [7], [8].

Overlap of [1] aabababaab=a with [1] aabababaab=a:

Critical pair: aabababa=aababaab.

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

Overlap of [1] aabababaab=a with [2] aabababa=aababaab:

Critical pair: aababaabab=a.

Referenced by [4], [5].

Overlap of [1] aabababaab=a with [2] aabababa=aababaab:

Critical pair: aabababaababaab=aababa.

Reduce LHS:

Flip LHS and RHS.

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

Simplify [3] aababaabab=a.

Reduce LHS:

Referenced by [6].

Overlap of [1] aabababaab=a with [5] aabaabaabb=a:

Critical pair: aabababa=aaabaabb.

Reduce LHS:

Referenced by [7], [8].

Overlap of [1] aabababaab=a with [4] aababa=aabaab:

Critical pair: aabaabbaab=a.

Reduce LHS:

Referenced by [8], [11].

Overlap of [1] aabababaab=a with [4] aababa=aabaab:

Critical pair: aabababaabaab=aaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

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

Overlap of [4] aababa=aabaab with [8] aaba=aaab:

Critical pair: aaabba=aabaab.

Reduce RHS:

Defines rule #2.

Referenced by [10], [12].

Overlap of [4] aababa=aabaab with [8] aaba=aaab:

Critical pair: aababaaab=aabaababa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [12].

Simplify [7] aaaabaabbb=a.

Reduce LHS:

Defines rule #4.

Referenced by [12].

Overlap of [2] aabababa=aababaab with [11] aaaaaabbbb=a:

Critical pair: aabababa=aababaabaaaaabbbb.

Reduce LHS:

Reduce RHS:

Defines rule #3.