Certificate for #22808 ⟨a, b | aaa=1, abbab=bba⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #8.

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

Axiom: abbab=bba.

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

Overlap of [1] aaa=1 with [2] abbab=bba:

Critical pair: aabba=bbab.

Referenced by [4], [5].

Overlap of [1] aaa=1 with [3] aabba=bbab:

Critical pair: aabbab=abba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6], [7], [17].

Overlap of [1] aaa=1 with [4] abba=bbabb:

Critical pair: aabbabb=bba.

Reduce LHS:

Defines rule #2.

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

Overlap of [2] abbab=bba with [4] abba=bbabb:

Critical pair: abbbbabb=bbaba.

Flip LHS and RHS.

Referenced by [13].

Overlap of [4] abba=bbabb with [1] aaa=1:

Critical pair: abb=bbabbaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [5] bbabbb=bba with [5] bbabbb=bba:

Critical pair: bbabbba=bbaabbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [9], [10].

Overlap of [5] bbabbb=bba with [8] bbaabbb=bbaa:

Critical pair: bbabbbaa=bbaaabbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [11], [13], [17].

Overlap of [8] bbaabbb=bbaa with [5] bbabbb=bba:

Critical pair: bbaabbbba=bbaababbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Simplify [7] bbbbbbabb=abb.

Reduce LHS:

Referenced by [12].

Overlap of [11] bbbabb=abb with [5] bbabbb=bba:

Critical pair: bbba=abbb.

Defines rule #3.

Referenced by [13], [15], [16], [17], [18].

Simplify [6] bbaba=abbbbabb.

Reduce RHS:

Defines rule #7.

Referenced by [14], [15], [17].

Overlap of [2] abbab=bba with [13] bbaba=ababb:

Critical pair: aababb=bbaa.

Defines rule #9.

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

Overlap of [12] bbba=abbb with [13] bbaba=ababb:

Critical pair: bababb=abbbba.

Reduce RHS:

Defines rule #5.

Overlap of [10] bbaababbb=bbaaba with [14] aababb=bbaa:

Critical pair: bbbbaab=bbaaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [18].

Overlap of [4] abba=bbabb with [14] aababb=bbaa:

Critical pair: abbbbaa=bbabbababb.

Reduce LHS:

Reduce RHS:

Referenced by [18].

Overlap of [14] aababb=bbaa with [12] bbba=abbb:

Critical pair: aabaabbb=bbaaba.

Reduce LHS:

Reduce RHS:

Defines rule #10.