Certificate for #22256 ⟨a, b | aaa=1, abaaba=bb⟩

Completion settings:

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

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [4], [7], [8], [9], [13], [14], [15], [16], [17], [20], [22], [23].

[2] abaaba=bb

Axiom: abaaba=bb.

Referenced by [6].

[3] bba=c

Axiom: bba=c.

Referenced by [4], [11].

[4] bb=caa

Overlap of [3] bba=c with [1] aaa=1:

bb a aaa

Critical pair: bb=caa.

Defines rule #2.

Referenced by [5], [6], [10], [13].

[5] caab=bcaa

Overlap of [4] bb=caa with [4] bb=caa:

b b bb

Critical pair: bcaa=caab.

Flip LHS and RHS.

Defines rule #7.

[6] abaaba=caa

Simplify [2] abaaba=bb.

Reduce RHS:

[4]	(bb)
	⇒ caa

Referenced by [7], [9].

[7] abaab=ca

Overlap of [6] abaaba=caa with [1] aaa=1:

abaab a aaa

Critical pair: abaab=caaaa.

Reduce RHS:

[1]	c(aaa)a
	⇒ ca

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

[8] baab=aaca

Overlap of [1] aaa=1 with [7] abaab=ca:

aa a abaab

Critical pair: aaca=baab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [11], [13].

[9] cb=abaca

Overlap of [6] abaaba=caa with [7] abaab=ca:

aba aba abaab

Critical pair: abaca=caaab.

Reduce RHS:

[1]	c(aaa)b
	⇒ cb

Flip LHS and RHS.

Defines rule #5.

Referenced by [16].

[10] cab=abaacaa

Overlap of [7] abaab=ca with [4] bb=caa:

abaa b bb

Critical pair: abaacaa=cab.

Flip LHS and RHS.

Referenced by [11], [12].

[11] abaacaa=baaca

Overlap of [3] bba=c with [8] baab=aaca:

b ba baab

Critical pair: baaca=cab.

Reduce RHS:

[10]	(cab)
	⇒ abaacaa

Flip LHS and RHS.

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

[12] cab=baaca

Simplify [10] cab=abaacaa.

Reduce RHS:

[11]	(abaacaa)
	⇒ baaca

Defines rule #6.

Referenced by [13], [16].

[13] aacca=cacaa

Overlap of [12] cab=baaca with [4] bb=caa:

ca b bb

Critical pair: cacaa=baacab.

Reduce RHS:

[12]	baa(cab)
[8]	⇒ (baab)aaca
[1]	⇒ aac(aaa)ca
	⇒ aacca

Flip LHS and RHS.

Referenced by [14].

[14] aacc=caca

Overlap of [13] aacca=cacaa with [1] aaa=1:

aacc a aaa

Critical pair: aacc=cacaaaa.

Reduce RHS:

[1]	cac(aaa)a
	⇒ caca

Defines rule #9.

Referenced by [15], [16], [21].

[15] acaca=cc

Overlap of [1] aaa=1 with [14] aacc=caca:

a aa aacc

Critical pair: acaca=cc.

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

[16] abacc=bcacaa

Overlap of [14] aacc=caca with [9] cb=abaca:

aac c cb

Critical pair: aacabaca=cacab.

Reduce LHS:

[12]	aa(cab)aca
[11]	⇒ a(abaacaa)ca
[15]	⇒ aba(acaca)
	⇒ abacc

Reduce RHS:

[12]	ca(cab)
[12]	⇒ (cab)aaca
[1]	⇒ baac(aaa)ca
[14]	⇒ b(aacc)a
	⇒ bcacaa

Defines rule #11.

Referenced by [19].

[17] acac=ccaa

Overlap of [15] acaca=cc with [1] aaa=1:

acac a aaa

Critical pair: acac=ccaa.

Defines rule #8.

[18] accc=ccca

Overlap of [15] acaca=cc with [15] acaca=cc:

ac aca acaca

Critical pair: accc=ccca.

Defines rule #12.

Referenced by [19].

[19] abccca=bcacaac

Overlap of [16] abacc=bcacaa with [18] accc=ccca:

ab acc accc

Critical pair: abccca=bcacaac.

Referenced by [23].

[20] abaac=baacaa

Overlap of [11] abaacaa=baaca with [1] aaa=1:

abaac aa aaa

Critical pair: abaac=baacaa.

Defines rule #4.

Referenced by [21].

[21] abcaca=baacaac

Overlap of [20] abaac=baacaa with [14] aacc=caca:

ab aac aacc

Critical pair: abcaca=baacaac.

Referenced by [22].

[22] abcac=baacaacaa

Overlap of [21] abcaca=baacaac with [1] aaa=1:

abcac a aaa

Critical pair: abcac=baacaacaa.

Defines rule #10.

[23] abccc=bcacaacaa

Overlap of [19] abccca=bcacaac with [1] aaa=1:

abccc a aaa

Critical pair: abccc=bcacaacaa.

Defines rule #13.