Certificate for #7462 ⟨a, b, c | ab=1, baaa=cc⟩

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], [8].

[2] cc=baaa

Axiom: baaa=cc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3].

[3] baaac=cbaaa

Overlap of [2] cc=baaa with [2] cc=baaa:

c c cc

Critical pair: cbaaa=baaac.

Flip LHS and RHS.

Referenced by [4], [5].

[4] aaac=acbaaa

Overlap of [1] ab=1 with [3] baaac=cbaaa:

a b baaac

Critical pair: acbaaa=aaac.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] bacbaaa=cbaaa

Overlap of [3] baaac=cbaaa with [4] aaac=acbaaa:

b aaac aaac

Critical pair: bacbaaa=cbaaa.

Referenced by [6].

[6] bacbaa=cbaa

Overlap of [5] bacbaaa=cbaaa with [1] ab=1:

bacbaa a ab

Critical pair: bacbaa=cbaaab.

Reduce RHS:

[1]	cbaa(ab)
	⇒ cbaa

Referenced by [7].

[7] bacba=cba

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

bacba a ab

Critical pair: bacba=cbaab.

Reduce RHS:

[1]	cba(ab)
	⇒ cba

Referenced by [8].

[8] bacb=cb

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

bacb a ab

Critical pair: bacb=cbab.

Reduce RHS:

[1]	cb(ab)
	⇒ cb

Defines rule #2.