Certificate for #4628 ⟨a, b | aaaa=a, babb=a⟩

Completion settings:

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

Axiom: aaaa=a.

Defines rule #4.

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

Axiom: babb=a.

Referenced by [3], [5], [7], [8], [9], [10], [14], [15], [16], [18].

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

Critical pair: baba=aabb.

Flip LHS and RHS.

Referenced by [4], [8], [13], [16].

Overlap of [1] aaaa=a with [3] aabb=baba:

Critical pair: aababa=abb.

Referenced by [5], [7].

Overlap of [4] aababa=abb with [2] babb=a:

Critical pair: aabaa=abbbb.

Referenced by [6], [7], [8].

Overlap of [5] aabaa=abbbb with [1] aaaa=a:

Critical pair: aaba=abbbbaa.

Referenced by [13].

Overlap of [5] aabaa=abbbb with [4] aababa=abb:

Critical pair: aababb=abbbbbaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [5] aabaa=abbbb with [5] aabaa=abbbb:

Critical pair: aababbbb=abbbbbaa.

Reduce LHS:

Referenced by [10], [12].

Overlap of [2] babb=a with [7] abbbbbaba=aaa:

Critical pair: baaa=abbbaba.

Flip LHS and RHS.

Referenced by [10].

Overlap of [2] babb=a with [9] abbbaba=baaa:

Critical pair: bbaaa=ababa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [10] abbbbbaa=bbaaa with [1] aaaa=a:

Critical pair: abbbbba=bbaaaaa.

Reduce RHS:

Referenced by [12], [14].

Simplify [8] ababa=abbbbbaa.

Reduce RHS:

Referenced by [13].

Overlap of [12] ababa=bbaaa with [6] aaba=abbbbaa:

Critical pair: abababbbbaa=bbaaaaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [2] babb=a with [11] abbbbba=bbaa:

Critical pair: bbbaa=abbba.

Flip LHS and RHS.

Referenced by [15].

Overlap of [2] babb=a with [14] abbba=bbbaa:

Critical pair: bbbbaa=aba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16].

Overlap of [15] aba=bbbbaa with [2] babb=a:

Critical pair: aa=bbbbaabb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [16] bbbbbbbbbaa=aa with [1] aaaa=a:

Critical pair: bbbbbbbbba=aaaa.

Reduce RHS:

Defines rule #1.

Referenced by [18].

Overlap of [17] bbbbbbbbba=a with [2] babb=a:

Critical pair: bbbbbbbba=abb.

Flip LHS and RHS.

Defines rule #2.