Certificate for #14585 ⟨a, b | aaba=a, bbaaa=a⟩

Completion settings:

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

[1] aaba=a

Axiom: aaba=a.

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

[2] bbaaa=a

Axiom: bbaaa=a.

Referenced by [4].

[3] bba=c

Axiom: bba=c.

Defines rule #9.

Referenced by [4], [5], [9], [13].

[4] caa=a

Overlap of [2] bbaaa=a with [3] bba=c:

bbaaa bba

Critical pair: caa=a.

Referenced by [6], [17].

[5] caba=c

Overlap of [3] bba=c with [1] aaba=a:

bb a aaba

Critical pair: bba=caba.

Reduce LHS:

[3]	(bba)
	⇒ c

Flip LHS and RHS.

Referenced by [7].

[6] aba=ca

Overlap of [4] caa=a with [1] aaba=a:

c aa aaba

Critical pair: ca=aba.

Flip LHS and RHS.

Referenced by [7], [10], [11], [18].

[7] abca=c

Overlap of [6] aba=ca with [6] aba=ca:

ab a aba

Critical pair: abca=caba.

Reduce RHS:

[5]	(caba)
	⇒ c

Referenced by [8], [9], [10], [11], [12], [14].

[8] aabc=c

Overlap of [1] aaba=a with [7] abca=c:

aab a abca

Critical pair: aabc=abca.

Reduce RHS:

[7]	(abca)
	⇒ c

Referenced by [15].

[9] bbc=cbca

Overlap of [3] bba=c with [7] abca=c:

bb a abca

Critical pair: bbc=cbca.

Referenced by [13], [19].

[10] abc=cc

Overlap of [6] aba=ca with [7] abca=c:

ab a abca

Critical pair: abc=cabca.

Reduce RHS:

[7]	c(abca)
	⇒ cc

Defines rule #5.

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

[11] cba=ccca

Overlap of [7] abca=c with [6] aba=ca:

abc a aba

Critical pair: abcca=cba.

Reduce LHS:

[10]	(abc)ca
	⇒ ccca

Flip LHS and RHS.

Referenced by [19], [20].

[12] cbca=ccc

Overlap of [7] abca=c with [7] abca=c:

abc a abca

Critical pair: abcc=cbca.

Reduce LHS:

[10]	(abc)c
	⇒ ccc

Flip LHS and RHS.

Referenced by [13].

[13] cbc=cccc

Overlap of [3] bba=c with [10] abc=cc:

bb a abc

Critical pair: bbcc=cbc.

Reduce LHS:

[9]	(bbc)c
[12]	⇒ (cbca)c
	⇒ cccc

Flip LHS and RHS.

Defines rule #3.

[14] cca=c

Overlap of [7] abca=c with [10] abc=cc:

abca abc

Critical pair: cca=c.

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

[15] acc=c

Simplify [8] aabc=c.

Reduce LHS:

[10]	a(abc)
	⇒ acc

Defines rule #1.

Referenced by [16].

[16] ca=ac

Overlap of [15] acc=c with [14] cca=c:

a cc cca

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #2.

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

[17] aac=a

Overlap of [4] caa=a with [16] ca=ac:

caa ca

Critical pair: aca=a.

Reduce LHS:

[16]	a(ca)
	⇒ aac

Defines rule #4.

[18] aba=ac

Simplify [6] aba=ca.

Reduce RHS:

[16]	(ca)
	⇒ ac

Defines rule #8.

[19] bbc=ccc

Simplify [9] bbc=cbca.

Reduce RHS:

[16]	cb(ca)
[11]	⇒ (cba)c
[14]	⇒ c(cca)c
	⇒ ccc

Defines rule #7.

[20] cba=cc

Simplify [11] cba=ccca.

Reduce RHS:

[14]	c(cca)
	⇒ cc

Defines rule #6.