Certificate for #4508 ⟨a, b | aaababaa=aab⟩

Completion settings:

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

[1] aaababaa=aab

Axiom: aaababaa=aab.

Referenced by [3].

[2] babaa=c

Axiom: babaa=c.

Defines rule #10.

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

[3] aab=aaac

Overlap of [1] aaababaa=aab with [2] babaa=c:

aaa babaa babaa

Critical pair: aaac=aab.

Flip LHS and RHS.

Defines rule #8.

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

[4] cb=cac

Overlap of [2] babaa=c with [3] aab=aaac:

bab aa aab

Critical pair: babaaac=cb.

Reduce LHS:

[2]	(babaa)ac
	⇒ cac

Flip LHS and RHS.

Defines rule #7.

Referenced by [7].

[5] cab=caac

Overlap of [2] babaa=c with [3] aab=aaac:

baba a aab

Critical pair: babaaaac=cab.

Reduce LHS:

[2]	(babaa)aac
	⇒ caac

Flip LHS and RHS.

Defines rule #9.

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

[6] aaacaacaa=aac

Overlap of [3] aab=aaac with [2] babaa=c:

aa b babaa

Critical pair: aac=aaacabaa.

Reduce RHS:

[5]	aaa(cab)aa
	⇒ aaacaacaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [9].

[7] cacaacaa=cc

Overlap of [4] cb=cac with [2] babaa=c:

c b babaa

Critical pair: cc=cacabaa.

Reduce RHS:

[5]	ca(cab)aa
	⇒ cacaacaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [10].

[8] caacaacaa=cac

Overlap of [5] cab=caac with [2] babaa=c:

ca b babaa

Critical pair: cac=caacabaa.

Reduce RHS:

[5]	caa(cab)aa
	⇒ caacaacaa

Flip LHS and RHS.

Defines rule #6.

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

[9] aaccaa=aaacac

Overlap of [6] aaacaacaa=aac with [8] caacaacaa=cac:

aaa caacaa caacaacaa

Critical pair: aaacac=aaccaa.

Flip LHS and RHS.

Defines rule #2.

[10] cccaa=cacac

Overlap of [7] cacaacaa=cc with [8] caacaacaa=cac:

ca caacaa caacaacaa

Critical pair: cacac=cccaa.

Flip LHS and RHS.

Defines rule #1.

[11] caccaa=caacac

Overlap of [8] caacaacaa=cac with [8] caacaacaa=cac:

caa caacaa caacaacaa

Critical pair: caacac=caccaa.

Flip LHS and RHS.

Defines rule #3.