Certificate for #7868 ⟨a, b, c | ab=1, ccc=baa⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(a) = deg(b) = 0, a < b; deg(c) = 1

[1] ab=1

Axiom: ab=1.

Defines rule #1.

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

[2] ccc=baa

Axiom: ccc=baa.

Defines rule #5.

Referenced by [3].

[3] baac=cbaa

Overlap of [2] ccc=baa with [2] ccc=baa:

c cc ccc

Critical pair: cbaa=baac.

Flip LHS and RHS.

Referenced by [4], [5].

[4] aac=acbaa

Overlap of [1] ab=1 with [3] baac=cbaa:

a b baac

Critical pair: acbaa=aac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] bacbaa=cbaa

Overlap of [3] baac=cbaa with [4] aac=acbaa:

b aac aac

Critical pair: bacbaa=cbaa.

Referenced by [6].

[6] bacba=cba

Overlap of [5] bacbaa=cbaa with [1] ab=1:

bacba a ab

Critical pair: bacba=cbaab.

Reduce RHS:

[1]	cba(ab)
	⇒ cba

Referenced by [7], [8].

[7] bacb=cb

Overlap of [6] bacba=cba with [1] ab=1:

bacb a ab

Critical pair: bacb=cbab.

Reduce RHS:

[1]	cb(ab)
	⇒ cb

Defines rule #3.

Referenced by [8].

[8] baccb=ccb

Overlap of [6] bacba=cba with [7] bacb=cb:

bac ba bacb

Critical pair: baccb=cbacb.

Reduce RHS:

[7]	c(bacb)
	⇒ ccb

Defines rule #4.