Certificate for #3535 ⟨a, b | aabaaaaaba=a⟩

Completion settings:

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

[1] aabaaaaaba=a

Axiom: aabaaaaaba=a.

Referenced by [4], [5], [7], [10], [12], [17].

[2] baaba=c

Axiom: baaba=c.

Defines rule #9.

Referenced by [3], [5], [6], [8], [12], [17].

[3] baac=caba

Overlap of [2] baaba=c with [2] baaba=c:

baa ba baaba

Critical pair: baac=caba.

Referenced by [6], [13], [22], [26].

[4] aabaaaa=aaaaaba

Overlap of [1] aabaaaaaba=a with [1] aabaaaaaba=a:

aabaaa aaba aabaaaaaba

Critical pair: aabaaaa=aaaaaba.

Referenced by [12], [17].

[5] caaaaba=ba

Overlap of [2] baaba=c with [1] aabaaaaaba=a:

b aaba aabaaaaaba

Critical pair: ba=caaaaba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [6], [7], [8], [22], [23], [32].

[6] cabaaaaaba=c

Overlap of [3] baac=caba with [5] caaaaba=ba:

baa c caaaaba

Critical pair: baaba=cabaaaaaba.

Reduce LHS:

[2]	(baaba)
	⇒ c

Flip LHS and RHS.

Referenced by [9].

[7] baaaaaba=caaa

Overlap of [5] caaaaba=ba with [1] aabaaaaaba=a:

caa aaba aabaaaaaba

Critical pair: caaa=baaaaaba.

Flip LHS and RHS.

Referenced by [9], [10].

[8] caaaac=c

Overlap of [5] caaaaba=ba with [2] baaba=c:

caaaa ba baaba

Critical pair: caaaac=baaba.

Reduce RHS:

[2]	(baaba)
	⇒ c

Referenced by [11].

[9] cacaaa=c

Simplify [6] cabaaaaaba=c.

Reduce LHS:

[7]	ca(baaaaaba)
	⇒ cacaaa

Referenced by [10], [11].

[10] cacaa=ccaaa

Overlap of [9] cacaaa=c with [1] aabaaaaaba=a:

caca aa aabaaaaaba

Critical pair: cacaa=cbaaaaaba.

Reduce RHS:

[7]	c(baaaaaba)
	⇒ ccaaa

Referenced by [11], [12], [14], [15].

[11] ccaaaa=c

Overlap of [8] caaaac=c with [9] cacaaa=c:

caaaa c cacaaa

Critical pair: caaaac=cacaaa.

Reduce LHS:

[8]	(caaaac)
	⇒ c

Reduce RHS:

[10]	(cacaa)a
	⇒ ccaaaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [15], [16], [20], [27].

[12] caac=caca

Overlap of [10] cacaa=ccaaa with [1] aabaaaaaba=a:

cac aa aabaaaaaba

Critical pair: caca=ccaaabaaaaaba.

Reduce RHS:

[4]	cca(aabaaaa)aba
[11]	⇒ (ccaaaa)aabaaba
[2]	⇒ caa(baaba)
	⇒ caac

Flip LHS and RHS.

Referenced by [13], [14], [15], [18].

[13] cabaaac=cacabaa

Overlap of [3] baac=caba with [12] caac=caca:

baa c caac

Critical pair: baacaca=cabaaac.

Reduce LHS:

[3]	(baac)aca
[3]	⇒ ca(baac)a
	⇒ cacabaa

Flip LHS and RHS.

Referenced by [19].

[14] ccaaac=cacaca

Overlap of [10] cacaa=ccaaa with [12] caac=caca:

ca caa caac

Critical pair: cacaca=ccaaac.

Flip LHS and RHS.

Referenced by [15].

[15] caccaaa=cc

Overlap of [12] caac=caca with [12] caac=caca:

caa c caac

Critical pair: caacaca=cacaaac.

Reduce LHS:

[12]	(caac)aca
[10]	⇒ (cacaa)ca
[14]	⇒ (ccaaac)a
[10]	⇒ ca(cacaa)
	⇒ caccaaa

Reduce RHS:

[10]	(cacaa)ac
[11]	⇒ (ccaaaa)c
	⇒ cc

Referenced by [16].

[16] cac=cca

Overlap of [15] caccaaa=cc with [11] ccaaaa=c:

ca ccaaa ccaaaa

Critical pair: cac=cca.

Defines rule #2.

Referenced by [18], [19], [21], [25], [27].

[17] aaaaac=a

Overlap of [1] aabaaaaaba=a with [4] aabaaaa=aaaaaba:

aabaaaaaba aabaaaa

Critical pair: aaaaabaaba=a.

Reduce LHS:

[2]	aaaaa(baaba)
	⇒ aaaaac

Referenced by [20], [21].

[18] caac=ccaa

Simplify [12] caac=caca.

Reduce RHS:

[16]	(cac)a
	⇒ ccaa

Referenced by [26].

[19] cabaaac=ccaabaa

Simplify [13] cabaaac=cacabaa.

Reduce RHS:

[16]	(cac)abaa
	⇒ ccaabaa

Referenced by [24].

[20] acaaaa=a

Overlap of [17] aaaaac=a with [11] ccaaaa=c:

aaaaa c ccaaaa

Critical pair: aaaaac=acaaaa.

Reduce LHS:

[17]	(aaaaac)
	⇒ a

Flip LHS and RHS.

Defines rule #3.

Referenced by [23], [31].

[21] aac=aca

Overlap of [17] aaaaac=a with [16] cac=cca:

aaaaa c cac

Critical pair: aaaaacca=aac.

Reduce LHS:

[17]	(aaaaac)ca
	⇒ aca

Flip LHS and RHS.

Defines rule #1.

Referenced by [22], [24], [25], [26], [27], [28], [29], [30], [31].

[22] baca=caba

Overlap of [5] caaaaba=ba with [21] aac=aca:

caaaab a aac

Critical pair: caaaabaca=baac.

Reduce LHS:

[5]	(caaaaba)ca
	⇒ baca

Reduce RHS:

[3]	(baac)
	⇒ caba

Defines rule #7.

Referenced by [23].

[23] cabaaaa=ba

Overlap of [5] caaaaba=ba with [20] acaaaa=a:

caaaab a acaaaa

Critical pair: caaaaba=bacaaaa.

Reduce LHS:

[5]	(caaaaba)
	⇒ ba

Reduce RHS:

[22]	(baca)aaa
	⇒ cabaaaa

Flip LHS and RHS.

Referenced by [24].

[24] ccaabaaa=bac

Overlap of [23] cabaaaa=ba with [21] aac=aca:

cabaa aa aac

Critical pair: cabaaaca=bac.

Reduce LHS:

[19]	(cabaaac)a
	⇒ ccaabaaa

Referenced by [25], [26].

[25] accaaabaaa=aabac

Overlap of [21] aac=aca with [24] ccaabaaa=bac:

aa c ccaabaaa

Critical pair: aabac=acacaabaaa.

Reduce RHS:

[16]	a(cac)aabaaa
	⇒ accaaabaaa

Flip LHS and RHS.

Referenced by [27].

[26] bacc=cccaaabaa

Overlap of [24] ccaabaaa=bac with [21] aac=aca:

ccaaba aa aac

Critical pair: ccaabaaca=bacc.

Reduce LHS:

[3]	ccaa(baac)a
[18]	⇒ c(caac)abaa
	⇒ cccaaabaa

Flip LHS and RHS.

Defines rule #8.

[27] acbaaa=aaabac

Overlap of [21] aac=aca with [25] accaaabaaa=aabac:

a ac accaaabaaa

Critical pair: aaabac=acacaaabaaa.

Reduce RHS:

[16]	a(cac)aaabaaa
[11]	⇒ a(ccaaaa)baaa
	⇒ acbaaa

Flip LHS and RHS.

Referenced by [28].

[28] acabaaa=aaaabac

Overlap of [21] aac=aca with [27] acbaaa=aaabac:

a ac acbaaa

Critical pair: aaaabac=acabaaa.

Flip LHS and RHS.

Referenced by [29].

[29] acaabaaa=aaaaabac

Overlap of [21] aac=aca with [28] acabaaa=aaaabac:

a ac acabaaa

Critical pair: aaaaabac=acaabaaa.

Flip LHS and RHS.

Referenced by [30].

[30] acaaabaaa=aaaaaabac

Overlap of [21] aac=aca with [29] acaabaaa=aaaaabac:

a ac acaabaaa

Critical pair: aaaaaabac=acaaabaaa.

Flip LHS and RHS.

Referenced by [31].

[31] abaaa=aaaaaaabac

Overlap of [21] aac=aca with [30] acaaabaaa=aaaaaabac:

a ac acaaabaaa

Critical pair: aaaaaaabac=acaaaabaaa.

Reduce RHS:

[20]	(acaaaa)baaa
	⇒ abaaa

Flip LHS and RHS.

Referenced by [32].

[32] baaa=caaaaaaaaaabac

Overlap of [5] caaaaba=ba with [31] abaaa=aaaaaaabac:

caaa aba abaaa

Critical pair: caaaaaaaaaabac=baaa.

Flip LHS and RHS.

Defines rule #6.