Certificate for #4711 ⟨a, b | aabbabba=baa⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(a) = deg(e) = 0, a < e; deg(d) = 1; deg(c) = 2; deg(b) = 3
• Auxiliary generators:
  1. bba=c
  2. cccc=d
  3. da=e

Axiom: aabbabba=baa.

Referenced by [5].

Axiom: bba=c.

Defines rule #12.

Referenced by [5], [8].

Axiom: cccc=d.

Defines rule #8.

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

Axiom: da=e.

Defines rule #3.

Referenced by [7], [9], [10], [11], [12], [13], [14].

Overlap of [1] aabbabba=baa with [2] bba=c:

Critical pair: aacbba=baa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

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

Overlap of [3] cccc=d with [3] cccc=d:

Critical pair: cd=dc.

Defines rule #7.

Referenced by [7], [11].

Overlap of [6] cd=dc with [4] da=e:

Critical pair: ce=dca.

Referenced by [11], [14].

Overlap of [2] bba=c with [5] baa=aacc:

Critical pair: baacc=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [9], [11], [12], [14].

Overlap of [3] cccc=d with [8] ca=aad:

Critical pair: cccaad=da.

Reduce LHS:

Reduce RHS:

Defines rule #2.

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

Overlap of [4] da=e with [9] aaeeed=e:

Critical pair: de=eaeeed.

Defines rule #4.

Referenced by [11], [12].

Overlap of [5] baa=aacc with [9] aaeeed=e:

Critical pair: be=aacceeed.

Reduce RHS:

Defines rule #9.

Overlap of [5] baa=aacc with [9] aaeeed=e:

Critical pair: bae=aaccaeeed.

Reduce RHS:

Defines rule #11.

Overlap of [9] aaeeed=e with [4] da=e:

Critical pair: aaeeee=ea.

Defines rule #1.

Simplify [7] ce=dca.

Reduce RHS:

Defines rule #6.