Certificate for #4230 ⟨a, b | abaaaaaba=ab⟩

Completion settings:

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

[1] abaaaaaba=ab

Axiom: abaaaaaba=ab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #7.

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

[3] abaaaaaba=c

Simplify [1] abaaaaaba=ab.

Reduce RHS:

[2]	(ab)
	⇒ c

Referenced by [4].

[4] caaaaca=c

Overlap of [3] abaaaaaba=c with [2] ab=c:

abaaaaaba ab

Critical pair: caaaaaba=c.

Reduce LHS:

[2]	caaaa(ab)a
	⇒ caaaaca

Referenced by [5], [6], [8], [9], [11], [12].

[5] cb=caaaacc

Overlap of [4] caaaaca=c with [2] ab=c:

caaaac a ab

Critical pair: caaaacc=cb.

Flip LHS and RHS.

Referenced by [7].

[6] caaaac=caaaca

Overlap of [4] caaaaca=c with [4] caaaaca=c:

caaaa ca caaaaca

Critical pair: caaaac=caaaca.

Referenced by [7], [8], [9], [11], [12], [14], [16], [18], [19].

[7] cb=caaacac

Simplify [5] cb=caaaacc.

Reduce RHS:

[6]	(caaaac)c
	⇒ caaacac

Referenced by [18].

[8] caaacaa=c

Overlap of [4] caaaaca=c with [6] caaaac=caaaca:

caaaaca caaaac

Critical pair: caaacaa=c.

Referenced by [9], [10].

[9] caaac=caaca

Overlap of [4] caaaaca=c with [6] caaaac=caaaca:

caaaa ca caaaac

Critical pair: caaaacaaaca=caaac.

Reduce LHS:

[6]	(caaaac)aaaca
[8]	⇒ (caaacaa)aaca
	⇒ caaca

Flip LHS and RHS.

Referenced by [10], [11], [12], [13], [14], [18], [19], [20].

[10] caacaaa=c

Simplify [8] caaacaa=c.

Reduce LHS:

[9]	(caaac)aa
	⇒ caacaaa

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

[11] caacaa=cacaaa

Overlap of [4] caaaaca=c with [10] caacaaa=c:

caaaa ca caacaaa

Critical pair: caaaac=cacaaa.

Reduce LHS:

[6]	(caaaac)
[9]	⇒ (caaac)a
	⇒ caacaa

Referenced by [12], [13], [14].

[12] cacaaaaaca=caac

Overlap of [4] caaaaca=c with [9] caaac=caaca:

caaaa ca caaac

Critical pair: caaaacaaca=caac.

Reduce LHS:

[6]	(caaaac)aaca
[9]	⇒ (caaac)aaaca
[11]	⇒ (caacaa)aaca
	⇒ cacaaaaaca

Referenced by [21].

[13] cacacaaa=cc

Overlap of [10] caacaaa=c with [9] caaac=caaca:

caa caaa caaac

Critical pair: caacaaca=cc.

Reduce LHS:

[11]	(caacaa)ca
[9]	⇒ ca(caaac)a
[11]	⇒ ca(caacaa)
	⇒ cacacaaa

Referenced by [14].

[14] caaca=ccaaa

Overlap of [9] caaac=caaca with [10] caacaaa=c:

caaa c caacaaa

Critical pair: caaac=caacaaacaaa.

Reduce LHS:

[9]	(caaac)
	⇒ caaca

Reduce RHS:

[11]	(caacaa)acaaa
[6]	⇒ ca(caaaac)aaa
[9]	⇒ ca(caaac)aaaa
[11]	⇒ ca(caacaa)aaa
[13]	⇒ (cacacaaa)aaa
	⇒ ccaaa

Referenced by [15], [16], [18], [19], [20].

[15] ccaaaaa=c

Overlap of [10] caacaaa=c with [14] caaca=ccaaa:

caacaaa caaca

Critical pair: ccaaaaa=c.

Defines rule #5.

Referenced by [16], [21].

[16] cac=cca

Overlap of [14] caaca=ccaaa with [6] caaaac=caaaca:

caa ca caaaac

Critical pair: caacaaaca=ccaaaaaac.

Reduce LHS:

[14]	(caaca)aaca
[15]	⇒ (ccaaaaa)ca
	⇒ cca

Reduce RHS:

[15]	(ccaaaaa)ac
	⇒ cac

Flip LHS and RHS.

Defines rule #1.

Referenced by [17], [21].

[17] ccaac=cccaa

Overlap of [16] cac=cca with [16] cac=cca:

ca c cac

Critical pair: cacca=ccaac.

Reduce LHS:

[16]	(cac)ca
[16]	⇒ c(cac)a
	⇒ cccaa

Flip LHS and RHS.

Referenced by [18].

[18] cb=cccaaaa

Simplify [7] cb=caaacac.

Reduce RHS:

[9]	(caaac)ac
[14]	⇒ (caaca)ac
[6]	⇒ c(caaaac)
[9]	⇒ c(caaac)a
[17]	⇒ (ccaac)aa
	⇒ cccaaaa

Defines rule #6.

[19] caaaac=ccaaaa

Simplify [6] caaaac=caaaca.

Reduce RHS:

[9]	(caaac)a
[14]	⇒ (caaca)a
	⇒ ccaaaa

Defines rule #4.

[20] caaac=ccaaa

Simplify [9] caaac=caaca.

Reduce RHS:

[14]	(caaca)
	⇒ ccaaa

Defines rule #3.

[21] caac=ccaa

Overlap of [12] cacaaaaaca=caac with [16] cac=cca:

cacaaaaaca cac

Critical pair: ccaaaaaaca=caac.

Reduce LHS:

[15]	(ccaaaaa)aca
[16]	⇒ (cac)a
	⇒ ccaa

Flip LHS and RHS.

Defines rule #2.