Certificate for #6824 ⟨a, b | aab=b, bbb=aaa⟩

Completion settings:

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

Axiom: aab=b.

Referenced by [3], [6], [7], [12].

Axiom: bbb=aaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

Overlap of [2] aaa=bbb with [1] aab=b:

Critical pair: ab=bbbb.

Flip LHS and RHS.

Referenced by [5], [7], [9], [10], [11], [13].

Overlap of [2] aaa=bbb with [2] aaa=bbb:

Critical pair: abbb=bbba.

Referenced by [8].

Overlap of [3] bbbb=ab with [3] bbbb=ab:

Critical pair: bab=abb.

Flip LHS and RHS.

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

Overlap of [1] aab=b with [5] abb=bab:

Critical pair: abab=bb.

Referenced by [9].

Overlap of [5] abb=bab with [3] bbbb=ab:

Critical pair: aab=babbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [11].

Simplify [4] abbb=bbba.

Reduce LHS:

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

Overlap of [3] bbbb=ab with [8] bbab=bbba:

Critical pair: bbbbba=abab.

Reduce LHS:

Reduce RHS:

Referenced by [10].

Overlap of [3] bbbb=ab with [8] bbab=bbba:

Critical pair: bbbbbba=abbab.

Reduce LHS:

Reduce RHS:

Referenced by [11].

Overlap of [5] abb=bab with [8] bbab=bbba:

Critical pair: abbbba=babbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [12], [13].

Overlap of [1] aab=b with [11] ab=ba:

Critical pair: aba=b.

Reduce LHS:

Defines rule #2.

Simplify [3] bbbb=ab.

Reduce RHS:

Defines rule #4.