Certificate for #5631 ⟨a, b, c | aa=a, abc=ca⟩

Completion settings:

Auxiliary generators:
1. d = bcb
Reduction order:
- Right-to-left recursive path with deg(a) = deg(b) = deg(d) = 0, a < b < d; deg(c) = 1

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [5].

[2] ca=abc

Axiom: abc=ca.

Flip LHS and RHS.

Defines rule #5.

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

[3] bcb=d

Axiom: bcb=d.

Defines rule #6.

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

[4] bcd=dcb

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

bc b bcb

Critical pair: bcd=dcb.

Defines rule #8.

Referenced by [8], [9].

[5] ababc=abc

Overlap of [2] ca=abc with [1] aa=a:

c a aa

Critical pair: ca=abca.

Reduce LHS:

[2]	(ca)
	⇒ abc

Reduce RHS:

[2]	ab(ca)
	⇒ ababc

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7].

[6] adabc=adc

Overlap of [2] ca=abc with [5] ababc=abc:

c a ababc

Critical pair: cabc=abcbabc.

Reduce LHS:

[2]	(ca)bc
[3]	⇒ a(bcb)c
	⇒ adc

Reduce RHS:

[3]	a(bcb)abc
	⇒ adabc

Flip LHS and RHS.

Defines rule #4.

Referenced by [9].

[7] abad=ad

Overlap of [5] ababc=abc with [3] bcb=d:

aba bc bcb

Critical pair: abad=abcb.

Reduce RHS:

[3]	a(bcb)
	⇒ ad

Defines rule #2.

Referenced by [8].

[8] adcb=adad

Overlap of [2] ca=abc with [7] abad=ad:

c a abad

Critical pair: cad=abcbad.

Reduce LHS:

[2]	(ca)d
[4]	⇒ a(bcd)
	⇒ adcb

Reduce RHS:

[3]	a(bcb)ad
	⇒ adad

Defines rule #7.

Referenced by [9].

[9] adcd=adadad

Overlap of [6] adabc=adc with [4] bcd=dcb:

ada bc bcd

Critical pair: adadcb=adcd.

Reduce LHS:

[8]	ad(adcb)
	⇒ adadad

Flip LHS and RHS.

Defines rule #9.