Certificate for #4887 ⟨a, b | abbbbbba=bab⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with b < a < c < d < e < f < g < h
• Auxiliary generators:
  1. ab=c
  2. cb=d
  3. db=e
  4. eb=f
  5. fb=g
  6. gb=h

Axiom: abbbbbba=bab.

Referenced by [8].

Axiom: ab=c.

Defines rule #1.

Referenced by [8], [9], [10], [16].

Axiom: cb=d.

Defines rule #2.

Referenced by [9], [10], [11], [17].

Axiom: db=e.

Defines rule #3.

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

Axiom: eb=f.

Defines rule #4.

Referenced by [9], [12], [13], [19].

Axiom: fb=g.

Defines rule #5.

Referenced by [9], [13], [14], [20].

Axiom: gb=h.

Defines rule #6.

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

Simplify [1] abbbbbba=bab.

Reduce RHS:

Referenced by [9].

Overlap of [8] abbbbbba=bc with [2] ab=c:

Critical pair: cbbbbba=bc.

Reduce LHS:

Defines rule #7.

Referenced by [10].

Overlap of [9] ha=bc with [2] ab=c:

Critical pair: hc=bcb.

Reduce RHS:

Defines rule #8.

Referenced by [11].

Overlap of [10] hc=bd with [3] cb=d:

Critical pair: hd=bdb.

Reduce RHS:

Defines rule #9.

Referenced by [12].

Overlap of [11] hd=be with [4] db=e:

Critical pair: he=beb.

Reduce RHS:

Defines rule #10.

Referenced by [13].

Overlap of [12] he=bf with [5] eb=f:

Critical pair: hf=bfb.

Reduce RHS:

Defines rule #11.

Referenced by [14].

Overlap of [13] hf=bg with [6] fb=g:

Critical pair: hg=bgb.

Reduce RHS:

Defines rule #12.

Referenced by [15].

Overlap of [14] hg=bh with [7] gb=h:

Critical pair: hh=bhb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [16], [17], [18], [19], [20], [21].

Overlap of [2] ab=c with [15] bhb=hh:

Critical pair: ahh=chb.

Flip LHS and RHS.

Defines rule #14.

Overlap of [3] cb=d with [15] bhb=hh:

Critical pair: chh=dhb.

Flip LHS and RHS.

Defines rule #15.

Overlap of [4] db=e with [15] bhb=hh:

Critical pair: dhh=ehb.

Flip LHS and RHS.

Defines rule #16.

Overlap of [5] eb=f with [15] bhb=hh:

Critical pair: ehh=fhb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [6] fb=g with [15] bhb=hh:

Critical pair: fhh=ghb.

Flip LHS and RHS.

Defines rule #18.

Overlap of [7] gb=h with [15] bhb=hh:

Critical pair: ghh=hhb.

Flip LHS and RHS.

Defines rule #19.