Certificate for #10767 ⟨a, b | aaab=bba, bbbb=1⟩

Completion settings:

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

Axiom: aaab=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4], [7], [8], [11], [20], [24].

Axiom: bbbb=1.

Defines rule #12.

Referenced by [3], [5], [23].

Overlap of [2] bbbb=1 with [1] bba=aaab:

Critical pair: bbaaab=a.

Reduce LHS:

Referenced by [4], [5], [6], [11], [12].

Overlap of [3] aaabaab=a with [1] bba=aaab:

Critical pair: aaabaaaaab=aba.

Referenced by [9], [10], [12], [16], [20], [25].

Overlap of [3] aaabaab=a with [2] bbbb=1:

Critical pair: aaabaa=abbb.

Flip LHS and RHS.

Referenced by [6], [7], [9], [23], [26].

Overlap of [3] aaabaab=a with [5] abbb=aaabaa:

Critical pair: aaabaaaabaa=abb.

Referenced by [11].

Overlap of [5] abbb=aaabaa with [1] bba=aaab:

Critical pair: abaaab=aaabaaa.

Defines rule #7.

Referenced by [8], [10], [13], [14], [17].

Overlap of [7] abaaab=aaabaaa with [1] bba=aaab:

Critical pair: abaaaaaab=aaabaaaba.

Reduce RHS:

Defines rule #10.

Referenced by [17], [18].

Overlap of [4] aaabaaaaab=aba with [5] abbb=aaabaa:

Critical pair: aaabaaaaaaabaa=ababb.

Flip LHS and RHS.

Referenced by [18].

Overlap of [4] aaabaaaaab=aba with [7] abaaab=aaabaaa:

Critical pair: aaabaaaaaaabaaa=abaaaab.

Referenced by [19].

Overlap of [6] aaabaaaabaa=abb with [6] aaabaaaabaa=abb:

Critical pair: aaabaabb=abbaabaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13], [15].

Overlap of [4] aaabaaaaab=aba with [11] aaaababaa=ab:

Critical pair: aaabaab=abaabaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [14], [15], [21], [22].

Overlap of [11] aaaababaa=ab with [7] abaaab=aaabaaa:

Critical pair: aaaabaaabaaa=abab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [15], [18], [20], [21].

Overlap of [12] abaabaa=a with [7] abaaab=aaabaaa:

Critical pair: abaaaabaaa=aab.

Referenced by [16], [17].

Overlap of [12] abaabaa=a with [11] aaaababaa=ab:

Critical pair: abaabab=aaababaa.

Reduce LHS:

Reduce RHS:

Referenced by [21].

Overlap of [14] abaaaabaaa=aab with [4] aaabaaaaab=aba:

Critical pair: abaaba=aabaab.

Flip LHS and RHS.

Referenced by [21].

Overlap of [14] abaaaabaaa=aab with [7] abaaab=aaabaaa:

Critical pair: abaaaaaabaaa=aabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [9] ababb=aaabaaaaaaabaa with [13] abab=aaaaaabaaaaaa:

Critical pair: aaaaaabaaaaaab=aaabaaaaaaabaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [10] aaabaaaaaaabaaa=abaaaab with [18] aaabaaaaaaabaa=aaaaaaaaaabaaaa:

Critical pair: aaaaaaaaaabaaaaa=abaaaab.

Flip LHS and RHS.

Referenced by [28].

Overlap of [1] bba=aaab with [13] abab=aaaaaabaaaaaa:

Critical pair: bbaaaaaabaaaaaa=aaabbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [16] aabaab=abaaba with [13] abab=aaaaaabaaaaaa:

Critical pair: aabaaaaaaabaaaaaa=abaabaab.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [22], [23], [24].

Overlap of [12] abaabaa=a with [21] abaaaaaaaa=ab:

Critical pair: abaab=aaaaaaa.

Defines rule #6.

Referenced by [23].

Overlap of [21] abaaaaaaaa=ab with [5] abbb=aaabaa:

Critical pair: abaaaaaaaaaabaa=abbbb.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [25], [26], [27], [28].

Overlap of [21] abaaaaaaaa=ab with [21] abaaaaaaaa=ab:

Critical pair: abaaaaaaaab=abbaaaaaaaa.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [26].

Overlap of [23] aaaaaaaaa=a with [4] aaabaaaaab=aba:

Critical pair: aaaaaaaba=abaaaaab.

Flip LHS and RHS.

Defines rule #9.

Overlap of [23] aaaaaaaaa=a with [5] abbb=aaabaa:

Critical pair: aaaaaaaaaaabaa=abbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [23] aaaaaaaaa=a with [26] aaaabaaaaaaab=aaabaa:

Critical pair: aaaaaaaabaa=abaaaaaaab.

Flip LHS and RHS.

Defines rule #11.

Simplify [19] abaaaab=aaaaaaaaaabaaaaa.

Reduce RHS:

Defines rule #8.