Certificate for #5385 ⟨a, b | abbaaab=abaa⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b < c
Auxiliary generators:
1. abaa=c

[1] abbaaab=abaa

Axiom: abbaaab=abaa.

Referenced by [3].

[2] abaa=c

Axiom: abaa=c.

Defines rule #1.

Referenced by [3], [4], [6], [7], [9], [10], [15], [17].

[3] abbaaab=c

Simplify [1] abbaaab=abaa.

Reduce RHS:

[2]	(abaa)
	⇒ c

Defines rule #11.

Referenced by [5], [6], [7], [8], [10], [13], [17].

[4] cbaa=abac

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

aba a abaa

Critical pair: abac=cbaa.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [13], [17].

[5] abbaac=abacab

Overlap of [3] abbaaab=c with [3] abbaaab=c:

abbaa ab abbaaab

Critical pair: abbaac=cbaaab.

Reduce RHS:

[4]	(cbaa)ab
	⇒ abacab

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

[6] abacab=caa

Overlap of [3] abbaaab=c with [2] abaa=c:

abbaa ab abaa

Critical pair: abbaac=caa.

Reduce LHS:

[5]	(abbaac)
	⇒ abacab

Defines rule #5.

Referenced by [8], [9], [10], [11], [13], [14], [16], [18].

[7] cbbaaab=abac

Overlap of [2] abaa=c with [3] abbaaab=c:

aba a abbaaab

Critical pair: abac=cbbaaab.

Flip LHS and RHS.

Defines rule #14.

Referenced by [17].

[8] cacab=caaaa

Overlap of [3] abbaaab=c with [6] abacab=caa:

abbaa ab abacab

Critical pair: abbaacaa=cacab.

Reduce LHS:

[5]	(abbaac)aa
[6]	⇒ (abacab)aa
	⇒ caaaa

Flip LHS and RHS.

Referenced by [10], [12].

[9] cbacab=abacaa

Overlap of [2] abaa=c with [6] abacab=caa:

aba a abacab

Critical pair: abacaa=cbacab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [17].

[10] caaaa=abacc

Overlap of [6] abacab=caa with [3] abbaaab=c:

abac ab abbaaab

Critical pair: abacc=caabaaab.

Reduce RHS:

[2]	ca(abaa)ab
[8]	⇒ (cacab)
	⇒ caaaa

Flip LHS and RHS.

Defines rule #3.

Referenced by [12].

[11] caaacab=abaccaa

Overlap of [6] abacab=caa with [6] abacab=caa:

abac ab abacab

Critical pair: abaccaa=caaacab.

Flip LHS and RHS.

Referenced by [13], [19].

[12] cacab=abacc

Simplify [8] cacab=caaaa.

Reduce RHS:

[10]	(caaaa)
	⇒ abacc

Defines rule #4.

Referenced by [13], [14].

[13] abaccaa=cacc

Overlap of [12] cacab=abacc with [3] abbaaab=c:

cac ab abbaaab

Critical pair: cacc=abaccbaaab.

Reduce RHS:

[4]	abac(cbaa)ab
[6]	⇒ (abacab)acab
[11]	⇒ (caaacab)
	⇒ abaccaa

Flip LHS and RHS.

Defines rule #10.

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

[14] caccaa=caaacc

Overlap of [12] cacab=abacc with [6] abacab=caa:

cac ab abacab

Critical pair: caccaa=abaccacab.

Reduce RHS:

[12]	abac(cacab)
[6]	⇒ (abacab)acc
	⇒ caaacc

Defines rule #7.

[15] cbaccaa=abacacc

Overlap of [2] abaa=c with [13] abaccaa=cacc:

aba a abaccaa

Critical pair: abacacc=cbaccaa.

Flip LHS and RHS.

Defines rule #13.

[16] caaaccaa=abaccacc

Overlap of [6] abacab=caa with [13] abaccaa=cacc:

abac ab abaccaa

Critical pair: abaccacc=caaaccaa.

Flip LHS and RHS.

Defines rule #15.

[17] cbbaac=abacaa

Overlap of [7] cbbaaab=abac with [3] abbaaab=c:

cbbaa ab abbaaab

Critical pair: cbbaac=abacbaaab.

Reduce RHS:

[4]	aba(cbaa)ab
[2]	⇒ (abaa)bacab
[9]	⇒ (cbacab)
	⇒ abacaa

Defines rule #9.

[18] abbaac=caa

Simplify [5] abbaac=abacab.

Reduce RHS:

[6]	(abacab)
	⇒ caa

Defines rule #6.

[19] caaacab=cacc

Simplify [11] caaacab=abaccaa.

Reduce RHS:

[13]	(abaccaa)
	⇒ cacc

Defines rule #12.