Certificate for #768 ⟨a, b | aaababaa=a⟩

Completion settings:

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

[1] aaababaa=a

Axiom: aaababaa=a.

Referenced by [3].

[2] aba=c

Axiom: aba=c.

Defines rule #1.

Referenced by [3], [4], [6], [7], [14], [15], [17], [19].

[3] aacbaa=a

Overlap of [1] aaababaa=a with [2] aba=c:

aa ababaa aba

Critical pair: aacbaa=a.

Referenced by [5].

[4] cba=abc

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

ab a aba

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [17].

[5] aaabca=a

Simplify [3] aacbaa=a.

Reduce LHS:

[4]	aa(cba)a
	⇒ aaabca

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

[6] caabca=c

Overlap of [2] aba=c with [5] aaabca=a:

ab a aaabca

Critical pair: aba=caabca.

Reduce LHS:

[2]	(aba)
	⇒ c

Flip LHS and RHS.

Referenced by [8], [9], [12], [18].

[7] aaabcc=c

Overlap of [5] aaabca=a with [2] aba=c:

aaabc a aba

Critical pair: aaabcc=aba.

Reduce RHS:

[2]	(aba)
	⇒ c

Referenced by [11].

[8] aaabc=aabca

Overlap of [5] aaabca=a with [6] caabca=c:

aaab ca caabca

Critical pair: aaabc=aabca.

Referenced by [10], [11].

[9] caabc=cabca

Overlap of [6] caabca=c with [6] caabca=c:

caab ca caabca

Critical pair: caabc=cabca.

Referenced by [18].

[10] aabcaa=a

Overlap of [5] aaabca=a with [8] aaabc=aabca:

aaabca aaabc

Critical pair: aabcaa=a.

Referenced by [12], [16].

[11] aabcac=c

Overlap of [7] aaabcc=c with [8] aaabc=aabca:

aaabcc aaabc

Critical pair: aabcac=c.

Referenced by [13].

[12] aabc=abca

Overlap of [10] aabcaa=a with [6] caabca=c:

aab caa caabca

Critical pair: aabc=abca.

Defines rule #3.

Referenced by [13], [15], [16], [17], [21], [22].

[13] abcaac=c

Simplify [11] aabcac=c.

Reduce LHS:

[12]	(aabc)ac
	⇒ abcaac

Referenced by [14], [22].

[14] cbcaac=abc

Overlap of [2] aba=c with [13] abcaac=c:

ab a abcaac

Critical pair: abc=cbcaac.

Flip LHS and RHS.

Referenced by [23].

[15] cabc=cbca

Overlap of [2] aba=c with [12] aabc=abca:

ab a aabc

Critical pair: ababca=cabc.

Reduce LHS:

[2]	(aba)bca
	⇒ cbca

Flip LHS and RHS.

Defines rule #5.

Referenced by [18], [23].

[16] abcaaa=a

Overlap of [10] aabcaa=a with [12] aabc=abca:

aabcaa aabc

Critical pair: abcaaa=a.

Referenced by [23].

[17] acbc=abcc

Overlap of [12] aabc=abca with [4] cba=abc:

aab c cba

Critical pair: aababc=abcaba.

Reduce LHS:

[2]	a(aba)bc
	⇒ acbc

Reduce RHS:

[2]	abc(aba)
	⇒ abcc

Defines rule #4.

Referenced by [19], [20].

[18] cbcaaa=c

Overlap of [6] caabca=c with [9] caabc=cabca:

caabca caabc

Critical pair: cabcaa=c.

Reduce LHS:

[15]	(cabc)aa
	⇒ cbcaaa

Referenced by [20].

[19] ccbc=cbcc

Overlap of [2] aba=c with [17] acbc=abcc:

ab a acbc

Critical pair: ababcc=ccbc.

Reduce LHS:

[2]	(aba)bcc
	⇒ cbcc

Flip LHS and RHS.

Defines rule #8.

[20] abccaaa=ac

Overlap of [17] acbc=abcc with [18] cbcaaa=c:

a cbc cbcaaa

Critical pair: ac=abccaaa.

Flip LHS and RHS.

Referenced by [21].

[21] abcacaaa=aac

Overlap of [12] aabc=abca with [20] abccaaa=ac:

a abc abccaaa

Critical pair: aac=abcacaaa.

Flip LHS and RHS.

Referenced by [22], [23].

[22] caaa=aaac

Overlap of [12] aabc=abca with [21] abcacaaa=aac:

a abc abcacaaa

Critical pair: aaac=abcaacaaa.

Reduce RHS:

[13]	(abcaac)aaa
	⇒ caaa

Flip LHS and RHS.

Defines rule #6.

[23] caac=a

Overlap of [15] cabc=cbca with [21] abcacaaa=aac:

c abc abcacaaa

Critical pair: caac=cbcaacaaa.

Reduce RHS:

[14]	(cbcaac)aaa
[16]	⇒ (abcaaa)
	⇒ a

Defines rule #7.