Certificate for #10739 ⟨a, b | aaab=baa, bbbb=1⟩

Completion settings:

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

Axiom: aaab=baa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [5], [6], [7], [8], [9], [11], [12], [17].

Axiom: bbbb=1.

Defines rule #6.

Referenced by [3], [4], [10], [13], [16], [18], [20].

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

Critical pair: bbbaaab=aa.

Reduce LHS:

Referenced by [4].

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

Critical pair: aaabababa=aabbb.

Referenced by [5], [6], [8], [19].

Overlap of [1] baa=aaab with [4] aaabababa=aabbb:

Critical pair: baaabbb=aaabaabababa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [4] aaabababa=aabbb with [1] baa=aaab:

Critical pair: aaababaaaab=aabbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7], [14].

Overlap of [6] aabbba=aaaaaaaaaaaababb with [1] baa=aaab:

Critical pair: aabbaaab=aaaaaaaaaaaababba.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [7] aaaaaaaaaaaababba=aaaaababab with [1] baa=aaab:

Critical pair: aaaaaaaaaaaababaaab=aaaaabababa.

Reduce LHS:

Reduce RHS:

Referenced by [9], [10].

Overlap of [8] aaaaaaaaaaaaaaaaaabbab=aaaabbb with [1] baa=aaab:

Critical pair: aaaaaaaaaaaaaaaaaabbaaaab=aaaabbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [11], [13].

Overlap of [8] aaaaaaaaaaaaaaaaaabbab=aaaabbb with [2] bbbb=1:

Critical pair: aaaaaaaaaaaaaaaaaabba=aaaabbbbbb.

Reduce RHS:

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

Overlap of [1] baa=aaab with [10] aaaaaaaaaaaaaaaaaabba=aaaabb:

Critical pair: baaaaabb=aaabaaaaaaaaaaaaaaaaabba.

Reduce LHS:

Reduce RHS:

Referenced by [14].

Overlap of [10] aaaaaaaaaaaaaaaaaabba=aaaabb with [1] baa=aaab:

Critical pair: aaaaaaaaaaaaaaaaaabaaab=aaaabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [15], [19], [21].

Overlap of [5] aaaaaabbababa=aaababbb with [12] aaaabba=aaaaaaaaaaaaaaaaaaaaabab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaababbaba=aaababbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Simplify [6] aabbba=aaaaaaaaaaaababb.

Reduce RHS:

Defines rule #5.

Referenced by [19].

Overlap of [10] aaaaaaaaaaaaaaaaaabba=aaaabb with [12] aaaabba=aaaaaaaaaaaaaaaaaaaaabab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabab=aaaabb.

Referenced by [16].

Overlap of [15] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabab=aaaabb with [2] bbbb=1:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaba=aaaabbbbb.

Reduce RHS:

Referenced by [17], [19], [22].

Overlap of [16] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaba=aaaab with [1] baa=aaab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab=aaaaba.

Flip LHS and RHS.

Referenced by [21].

Overlap of [13] aaababbb=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa with [2] bbbb=1:

Critical pair: aaaba=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab.

Referenced by [19].

Overlap of [4] aaabababa=aabbb with [18] aaaba=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabbaba=aabbb.

Reduce LHS:

Referenced by [20].

Overlap of [19] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabbb=aabbb with [2] bbbb=1:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=aabbbb.

Reduce RHS:

Defines rule #1.

Referenced by [21], [22].

Overlap of [20] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=aa with [12] aaaabba=aaaaaaaaaaaaaaaaaaaaabab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabab=aabba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Overlap of [20] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=aa with [16] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaba=aaaab:

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab=aaba.

Flip LHS and RHS.

Defines rule #2.