Certificate for #703 ⟨a, b | abaabaaab=1⟩

Completion settings:

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

[1] abaabaaab=1

Axiom: abaabaaab=1.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Referenced by [3], [4], [7], [9], [10], [13].

[3] abcac=1

Overlap of [1] abaabaaab=1 with [2] aab=c:

ab aabaaab aab

Critical pair: abcaaab=1.

Reduce LHS:

[2]	abca(aab)
	⇒ abcac

Referenced by [4], [5], [8], [10].

[4] ccac=a

Overlap of [2] aab=c with [3] abcac=1:

a ab abcac

Critical pair: a=ccac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6], [7], [16], [19], [20], [21], [22].

[5] abcaa=cac

Overlap of [3] abcac=1 with [4] ccac=a:

abca c ccac

Critical pair: abcaa=cac.

Referenced by [9], [10].

[6] ccaa=acac

Overlap of [4] ccac=a with [4] ccac=a:

cca c ccac

Critical pair: ccaa=acac.

Defines rule #1.

Referenced by [7], [18].

[7] acacab=a

Overlap of [6] ccaa=acac with [2] aab=c:

cca a aab

Critical pair: ccac=acacab.

Reduce LHS:

[4]	(ccac)
	⇒ a

Flip LHS and RHS.

Referenced by [8].

[8] acab=abca

Overlap of [3] abcac=1 with [7] acacab=a:

abc ac acacab

Critical pair: abca=acab.

Flip LHS and RHS.

Referenced by [10].

[9] cacb=abcc

Overlap of [5] abcaa=cac with [2] aab=c:

abc aa aab

Critical pair: abcc=cacb.

Flip LHS and RHS.

Referenced by [14].

[10] cabca=1

Overlap of [5] abcaa=cac with [2] aab=c:

abca a aab

Critical pair: abcac=cacab.

Reduce LHS:

[3]	(abcac)
	⇒ 1

Reduce RHS:

[8]	c(acab)
	⇒ cabca

Flip LHS and RHS.

Referenced by [11], [12].

[11] cab=bca

Overlap of [10] cabca=1 with [10] cabca=1:

cab ca cabca

Critical pair: cab=bca.

Referenced by [12], [15].

[12] bcaca=1

Overlap of [10] cabca=1 with [11] cab=bca:

cabca cab

Critical pair: bcaca=1.

Defines rule #3.

Referenced by [13], [17], [18], [19], [20], [22].

[13] ab=bcacc

Overlap of [12] bcaca=1 with [2] aab=c:

bcac a aab

Critical pair: bcacc=ab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [14], [15], [17], [18], [19], [20].

[14] cacb=bcacccc

Simplify [9] cacb=abcc.

Reduce RHS:

[13]	(ab)cc
	⇒ bcacccc

Referenced by [21].

[15] cbcacc=bca

Overlap of [11] cab=bca with [13] ab=bcacc:

c ab ab

Critical pair: cbcacc=bca.

Referenced by [16], [17], [19].

[16] cbcaa=bcaac

Overlap of [15] cbcacc=bca with [4] ccac=a:

cbca cc ccac

Critical pair: cbcaa=bcaac.

Referenced by [17].

[17] bcaacb=cbcc

Overlap of [16] cbcaa=bcaac with [13] ab=bcacc:

cbca a ab

Critical pair: cbcabcacc=bcaacb.

Reduce LHS:

[13]	cbc(ab)cacc
[15]	⇒ cb(cbcacc)cacc
[12]	⇒ cb(bcaca)cc
	⇒ cbcc

Flip LHS and RHS.

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

[18] caccb=acbcc

Overlap of [13] ab=bcacc with [17] bcaacb=cbcc:

a b bcaacb

Critical pair: acbcc=bcacccaacb.

Reduce RHS:

[6]	bcac(ccaa)cb
[12]	⇒ (bcaca)caccb
	⇒ caccb

Flip LHS and RHS.

Referenced by [21].

[19] cbcac=bccca

Overlap of [17] bcaacb=cbcc with [15] cbcacc=bca:

bcaa cb cbcacc

Critical pair: bcaabca=cbcccacc.

Reduce LHS:

[13]	bca(ab)ca
[13]	⇒ bc(ab)caccca
[15]	⇒ b(cbcacc)caccca
[12]	⇒ b(bcaca)ccca
	⇒ bccca

Reduce RHS:

[4]	cbc(ccac)c
	⇒ cbcac

Flip LHS and RHS.

Referenced by [20].

[20] cbca=bccccca

Overlap of [17] bcaacb=cbcc with [19] cbcac=bccca:

bcaa cb cbcac

Critical pair: bcaabccca=cbcccac.

Reduce LHS:

[13]	bca(ab)ccca
[13]	⇒ bc(ab)caccccca
[19]	⇒ b(cbcac)ccaccccca
[4]	⇒ bbc(ccac)caccccca
[12]	⇒ b(bcaca)ccccca
	⇒ bccccca

Reduce RHS:

[4]	cbc(ccac)
	⇒ cbca

Flip LHS and RHS.

Referenced by [22].

[21] acb=bcacccccc

Overlap of [4] ccac=a with [18] caccb=acbcc:

c cac caccb

Critical pair: cacbcc=acb.

Reduce LHS:

[14]	(cacb)cc
	⇒ bcacccccc

Flip LHS and RHS.

Referenced by [22].

[22] cb=bcccc

Overlap of [12] bcaca=1 with [21] acb=bcacccccc:

bcac a acb

Critical pair: bcacbcacccccc=cb.

Reduce LHS:

[21]	bc(acb)cacccccc
[20]	⇒ b(cbca)cccccccacccccc
[4]	⇒ bbccc(ccac)ccccccacccccc
[4]	⇒ bbc(ccac)cccccacccccc
[4]	⇒ bbcaccc(ccac)ccccc
[4]	⇒ bbcac(ccac)cccc
[12]	⇒ b(bcaca)cccc
	⇒ bcccc

Flip LHS and RHS.

Defines rule #5.