Certificate for #5357 ⟨a, b | abababa=aaba⟩

Completion settings:

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

[1] abababa=aaba

Axiom: abababa=aaba.

Referenced by [3].

[2] aaba=c

Axiom: aaba=c.

Defines rule #4.

Referenced by [3], [4], [6], [7], [8], [9], [11], [13].

[3] abababa=c

Simplify [1] abababa=aaba.

Reduce RHS:

[2]	(aaba)
	⇒ c

Defines rule #13.

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

[4] caba=aabc

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

aab a aaba

Critical pair: aabc=caba.

Flip LHS and RHS.

Referenced by [6], [8], [9], [12], [13], [15], [21].

[5] cba=abc

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

ab ababa abababa

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [8], [9], [13], [14], [17].

[6] abababc=aabc

Overlap of [3] abababa=c with [2] aaba=c:

ababab a aaba

Critical pair: abababc=caba.

Reduce RHS:

[4]	(caba)
	⇒ aabc

Referenced by [19].

[7] ababc=ac

Overlap of [2] aaba=c with [3] abababa=c:

a aba abababa

Critical pair: ac=cbaba.

Reduce RHS:

[5]	(cba)ba
[5]	⇒ ab(cba)
	⇒ ababc

Flip LHS and RHS.

Defines rule #10.

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

[8] abcbc=cc

Overlap of [4] caba=aabc with [3] abababa=c:

c aba abababa

Critical pair: cc=aabcbaba.

Reduce RHS:

[5]	aab(cba)ba
[2]	⇒ (aaba)bcba
[5]	⇒ cb(cba)
[5]	⇒ (cba)bc
	⇒ abcbc

Flip LHS and RHS.

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

[9] abaabc=cbc

Overlap of [5] cba=abc with [2] aaba=c:

cb a aaba

Critical pair: cbc=abcaba.

Reduce RHS:

[4]	ab(caba)
	⇒ abaabc

Flip LHS and RHS.

Referenced by [15], [18].

[10] ababac=cbc

Overlap of [3] abababa=c with [7] ababc=ac:

abab aba ababc

Critical pair: ababac=cbc.

Referenced by [20].

[11] cbc=aac

Overlap of [2] aaba=c with [7] ababc=ac:

a aba ababc

Critical pair: aac=cbc.

Flip LHS and RHS.

Defines rule #2.

Referenced by [13], [14], [16], [18], [20].

[12] cac=acc

Overlap of [4] caba=aabc with [7] ababc=ac:

c aba ababc

Critical pair: cac=aabcbc.

Reduce RHS:

[8]	a(abcbc)
	⇒ acc

Defines rule #3.

[13] aaaac=aabcc

Overlap of [4] caba=aabc with [7] ababc=ac:

cab a ababc

Critical pair: cabac=aabcbabc.

Reduce LHS:

[4]	(caba)c
	⇒ aabcc

Reduce RHS:

[5]	aab(cba)bc
[2]	⇒ (aaba)bcbc
[11]	⇒ (cbc)bc
[11]	⇒ aa(cbc)
	⇒ aaaac

Flip LHS and RHS.

Referenced by [18].

[14] aaac=abcc

Overlap of [5] cba=abc with [7] ababc=ac:

cb a ababc

Critical pair: cbac=abcbabc.

Reduce LHS:

[5]	(cba)c
	⇒ abcc

Reduce RHS:

[5]	ab(cba)bc
[7]	⇒ (ababc)bc
[11]	⇒ a(cbc)
	⇒ aaac

Flip LHS and RHS.

Defines rule #6.

[15] aaabc=cc

Overlap of [7] ababc=ac with [4] caba=aabc:

abab c caba

Critical pair: ababaabc=acaba.

Reduce LHS:

[9]	ab(abaabc)
[8]	⇒ (abcbc)
	⇒ cc

Reduce RHS:

[4]	a(caba)
	⇒ aaabc

Flip LHS and RHS.

Referenced by [17].

[16] abaac=cc

Simplify [8] abcbc=cc.

Reduce LHS:

[11]	ab(cbc)
	⇒ abaac

Defines rule #11.

Referenced by [17], [18].

[17] cabc=abcc

Overlap of [16] abaac=cc with [5] cba=abc:

abaa c cba

Critical pair: abaaabc=ccba.

Reduce LHS:

[15]	ab(aaabc)
	⇒ abcc

Reduce RHS:

[5]	c(cba)
	⇒ cabc

Flip LHS and RHS.

Defines rule #8.

[18] caac=aacc

Overlap of [16] abaac=cc with [11] cbc=aac:

abaa c cbc

Critical pair: abaaaac=ccbc.

Reduce LHS:

[13]	ab(aaaac)
[9]	⇒ (abaabc)c
[11]	⇒ (cbc)c
	⇒ aacc

Reduce RHS:

[11]	c(cbc)
	⇒ caac

Flip LHS and RHS.

Defines rule #9.

[19] aabc=abac

Overlap of [6] abababc=aabc with [7] ababc=ac:

ab ababc ababc

Critical pair: abac=aabc.

Flip LHS and RHS.

Defines rule #5.

Referenced by [21].

[20] ababac=aac

Simplify [10] ababac=cbc.

Reduce RHS:

[11]	(cbc)
	⇒ aac

Defines rule #12.

[21] caba=abac

Simplify [4] caba=aabc.

Reduce RHS:

[19]	(aabc)
	⇒ abac

Defines rule #7.