Certificate for #6268 ⟨a, b | aaa=a, baabb=a⟩

Completion settings:

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

Axiom: aaa=a.

Defines rule #3.

Referenced by [3], [4], [5], [6], [7], [9], [10].

Axiom: baabb=a.

Referenced by [3], [4], [5], [8].

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

Critical pair: baaba=aaabb.

Reduce RHS:

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

Overlap of [2] baabb=a with [3] baaba=abb:

Critical pair: baababb=aaaba.

Reduce LHS:

Reduce RHS:

Referenced by [9].

Overlap of [3] baaba=abb with [2] baabb=a:

Critical pair: baaa=abbabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7], [10].

Overlap of [3] baaba=abb with [3] baaba=abb:

Critical pair: baaabb=abbaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [11].

Overlap of [1] aaa=a with [5] abbabb=ba:

Critical pair: aaba=abbabb.

Reduce RHS:

Referenced by [8], [12].

Overlap of [3] baaba=abb with [7] aaba=ba:

Critical pair: baabba=abbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [3] baaba=abb with [8] babb=aa:

Critical pair: baaaa=abbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [8] babb=aa with [5] abbabb=ba:

Critical pair: bba=aaabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [12].

Simplify [6] abbaba=babb.

Reduce RHS:

Referenced by [12].

Overlap of [11] abbaba=aa with [10] abb=bba:

Critical pair: bbaaba=aa.

Reduce LHS:

Defines rule #4.