Certificate for #4816 ⟨a, b | ababaaab=bab⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(c) = deg(d) = deg(a) = 0, c < d < a; deg(b) = 1
Auxiliary generators:
1. ab=c
2. aac=d

[1] ababaaab=bab

Axiom: ababaaab=bab.

Referenced by [4].

[2] ab=c

Axiom: ab=c.

Defines rule #8.

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

[3] aac=d

Axiom: aac=d.

Defines rule #2.

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

[4] ababaaab=bc

Simplify [1] ababaaab=bab.

Reduce RHS:

[2]	b(ab)
	⇒ bc

Referenced by [5].

[5] bc=ccd

Overlap of [4] ababaaab=bc with [2] ab=c:

ababaaab ab

Critical pair: cabaaab=bc.

Reduce LHS:

[2]	c(ab)aaab
[2]	⇒ ccaa(ab)
[3]	⇒ cc(aac)
	⇒ ccd

Flip LHS and RHS.

Defines rule #7.

Referenced by [6].

[6] accd=cc

Overlap of [2] ab=c with [5] bc=ccd:

a b bc

Critical pair: accd=cc.

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

[7] acc=dcd

Overlap of [3] aac=d with [6] accd=cc:

a ac accd

Critical pair: acc=dcd.

Defines rule #1.

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

[8] adcd=dc

Overlap of [3] aac=d with [7] acc=dcd:

a ac acc

Critical pair: adcd=dc.

Defines rule #4.

Referenced by [11].

[9] dcdd=cc

Overlap of [6] accd=cc with [7] acc=dcd:

accd acc

Critical pair: dcdd=cc.

Defines rule #3.

Referenced by [10], [11].

[10] dcdcc=cccdd

Overlap of [6] accd=cc with [9] dcdd=cc:

acc d dcdd

Critical pair: acccc=cccdd.

Reduce LHS:

[7]	(acc)cc
	⇒ dcdcc

Defines rule #5.

[11] adccc=dccdd

Overlap of [8] adcd=dc with [9] dcdd=cc:

adc d dcdd

Critical pair: adccc=dccdd.

Defines rule #6.