Certificate for #3914 ⟨a, b | aabb=ba, bbbb=1⟩

Completion settings:

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

Axiom: aabb=ba.

Referenced by [3], [4], [6], [7], [10], [18].

Axiom: bbbb=1.

Defines rule #8.

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

Overlap of [1] aabb=ba with [2] bbbb=1:

Critical pair: aa=babb.

Flip LHS and RHS.

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

Overlap of [1] aabb=ba with [3] babb=aa:

Critical pair: aabaa=baabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [2] bbbb=1 with [3] babb=aa:

Critical pair: bbbaa=abb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [24].

Overlap of [3] babb=aa with [3] babb=aa:

Critical pair: babaa=aaabb.

Reduce RHS:

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

Overlap of [1] aabb=ba with [4] bba=aabaa:

Critical pair: aaaabaa=baa.

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

Overlap of [2] bbbb=1 with [4] bba=aabaa:

Critical pair: bbaabaa=a.

Reduce LHS:

Referenced by [19].

Overlap of [3] babb=aa with [4] bba=aabaa:

Critical pair: baaabaa=aaa.

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

Overlap of [4] bba=aabaa with [1] aabb=ba:

Critical pair: bbba=aabaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [6] babaa=aba with [9] baaabaa=aaa:

Critical pair: baaaa=abaabaa.

Flip LHS and RHS.

Referenced by [18].

Overlap of [7] aaaabaa=baa with [9] baaabaa=aaa:

Critical pair: aaaaaaa=baaabaa.

Reduce RHS:

Referenced by [19].

Overlap of [9] baaabaa=aaa with [9] baaabaa=aaa:

Critical pair: baaaaaa=aaaabaa.

Reduce RHS:

Referenced by [14].

Overlap of [6] babaa=aba with [13] baaaaaa=baa:

Critical pair: babaa=abaaaaa.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [6] babaa=aba with [14] abaaaaa=aba:

Critical pair: baba=abaaaa.

Defines rule #4.

Referenced by [20], [23].

Overlap of [7] aaaabaa=baa with [14] abaaaaa=aba:

Critical pair: aaaaba=baaaaa.

Referenced by [21].

Overlap of [9] baaabaa=aaa with [14] abaaaaa=aba:

Critical pair: baaaba=aaaaaa.

Referenced by [19], [22].

Overlap of [1] aabb=ba with [5] abb=baabaaa:

Critical pair: abaabaaa=ba.

Reduce LHS:

Referenced by [21].

Overlap of [8] aabaaabaa=a with [17] baaaba=aaaaaa:

Critical pair: aaaaaaaaa=a.

Reduce LHS:

Defines rule #1.

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

Overlap of [10] aababa=baabaa with [15] baba=abaaaa:

Critical pair: aaabaaaa=baabaa.

Flip LHS and RHS.

Referenced by [24].

Simplify [16] aaaaba=baaaaa.

Reduce RHS:

Defines rule #2.

Referenced by [25].

Simplify [17] baaaba=aaaaaa.

Reduce RHS:

Defines rule #6.

Referenced by [23].

Overlap of [15] baba=abaaaa with [22] baaaba=aa:

Critical pair: baaa=abaaaaaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [25].

Simplify [5] abb=baabaaa.

Reduce RHS:

Defines rule #7.

Overlap of [21] aaaaba=ba with [23] abaaba=baaa:

Critical pair: aaabaaa=baaba.

Flip LHS and RHS.

Defines rule #5.