Certificate for #2908 ⟨a, b | aaabaaababa=1⟩

Back:⟨a, b | aaabaaababa=1⟩

Completion settings:

[1] aaabaaababa=1

Axiom: aaabaaababa=1.

Referenced by [3].

[2] aba=c

Axiom: aba=c.

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

[3] aacacba=1

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

aa abaaababa aba

Critical pair: aacaababa=1.

Reduce LHS:

[2]aaca(aba)ba
⇒ aacacba

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.

Referenced by [5], [7], [11], [14].

[5] aacaabc=1

Simplify [3] aacacba=1.

Reduce LHS:

[4]aaca(cba)
⇒ aacaabc

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

[6] cacaabc=ab

Overlap of [2] aba=c with [5] aacaabc=1:

ab a aacaabc

Critical pair: ab=cacaabc.

Flip LHS and RHS.

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

[7] ba=aacacbc

Overlap of [5] aacaabc=1 with [4] cba=abc:

aacaab c cba

Critical pair: aacaababc=ba.

Reduce LHS:

[2]aaca(aba)bc
⇒ aacacbc

Flip LHS and RHS.

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

[8] acaabc=aacacb

Overlap of [5] aacaabc=1 with [6] cacaabc=ab:

aacaab c cacaabc

Critical pair: aacaabab=acaabc.

Reduce LHS:

[2]aaca(aba)b
⇒ aacacb

Flip LHS and RHS.

Referenced by [11].

[9] ccaabc=cacacb

Overlap of [6] cacaabc=ab with [6] cacaabc=ab:

cacaab c cacaabc

Critical pair: cacaabab=abacaabc.

Reduce LHS:

[2]caca(aba)b
⇒ cacacb

Reduce RHS:

[2](aba)caabc
⇒ ccaabc

Flip LHS and RHS.

Referenced by [10].

[10] caabc=acacb

Overlap of [5] aacaabc=1 with [9] ccaabc=cacacb:

aacaab c ccaabc

Critical pair: aacaabcacacb=caabc.

Reduce LHS:

[5](aacaabc)acacb
⇒ acacb

Flip LHS and RHS.

Referenced by [11], [13], [16], [18].

[11] bc=caccacb

Overlap of [10] caabc=acacb with [10] caabc=acacb:

caab c caabc

Critical pair: caabacacb=acacbaabc.

Reduce LHS:

[2]ca(aba)cacb
⇒ caccacb

Reduce RHS:

[4]aca(cba)abc
[8]⇒ (acaabc)abc
[4]⇒ aaca(cba)bc
[5]⇒ (aacaabc)bc
⇒ bc

Flip LHS and RHS.

Defines rule #5.

Referenced by [12], [14], [15], [17], [18], [22], [25].

[12] aaacaccaccacb=c

Overlap of [2] aba=c with [7] ba=aacacbc:

a ba ba

Critical pair: aaacacbc=c.

Reduce LHS:

[11]aaacac(bc)
⇒ aaacaccaccacb

Referenced by [19], [21].

[13] aaacacb=1

Overlap of [5] aacaabc=1 with [10] caabc=acacb:

aa caabc caabc

Critical pair: aaacacb=1.

Referenced by [24], [26].

[14] cba=acaccacb

Simplify [4] cba=abc.

Reduce RHS:

[11]a(bc)
⇒ acaccacb

Referenced by [15].

[15] caacaccaccacb=acaccacb

Overlap of [14] cba=acaccacb with [7] ba=aacacbc:

c ba ba

Critical pair: caacacbc=acaccacb.

Reduce LHS:

[11]caacac(bc)
⇒ caacaccaccacb

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

[16] caacacb=ab

Overlap of [6] cacaabc=ab with [10] caabc=acacb:

ca caabc caabc

Critical pair: caacacb=ab.

Referenced by [20], [23].

[17] ba=aacaccaccacb

Simplify [7] ba=aacacbc.

Reduce RHS:

[11]aacac(bc)
⇒ aacaccaccacb

Defines rule #6.

Referenced by [19], [20], [21], [23], [24].

[18] caacaccacb=acacb

Overlap of [10] caabc=acacb with [11] bc=caccacb:

caa bc bc

Critical pair: caacaccacb=acacb.

Referenced by [19], [20], [22], [23], [25].

[19] aaacaccacacacb=ca

Overlap of [12] aaacaccaccacb=c with [17] ba=aacaccaccacb:

aaacaccaccac b ba

Critical pair: aaacaccaccacaacaccaccacb=ca.

Reduce LHS:

[15]aaacaccacca(caacaccaccacb)
[18]⇒ aaacaccac(caacaccacb)
⇒ aaacaccacacacb

Referenced by [20].

[20] aaacaccaab=caa

Overlap of [19] aaacaccacacacb=ca with [17] ba=aacaccaccacb:

aaacaccacacac b ba

Critical pair: aaacaccacacacaacaccaccacb=caa.

Reduce LHS:

[15]aaacaccacaca(caacaccaccacb)
[18]⇒ aaacaccaca(caacaccacb)
[16]⇒ aaacacca(caacacb)
⇒ aaacaccaab

Referenced by [21], [22].

[21] aaacaccac=caaa

Overlap of [20] aaacaccaab=caa with [17] ba=aacaccaccacb:

aaacaccaa b ba

Critical pair: aaacaccaaaacaccaccacb=caaa.

Reduce LHS:

[12]aaacacca(aaacaccaccacb)
⇒ aaacaccac

Referenced by [24].

[22] aaacacacacb=caac

Overlap of [20] aaacaccaab=caa with [11] bc=caccacb:

aaacaccaa b bc

Critical pair: aaacaccaacaccacb=caac.

Reduce LHS:

[18]aaacac(caacaccacb)
⇒ aaacacacacb

Referenced by [23].

[23] aaacaab=caaca

Overlap of [22] aaacacacacb=caac with [17] ba=aacaccaccacb:

aaacacacac b ba

Critical pair: aaacacacacaacaccaccacb=caaca.

Reduce LHS:

[15]aaacacaca(caacaccaccacb)
[18]⇒ aaacaca(caacaccacb)
[16]⇒ aaaca(caacacb)
⇒ aaacaab

Defines rule #4.

Referenced by [24], [25].

[24] aaacac=caacaa

Overlap of [23] aaacaab=caaca with [17] ba=aacaccaccacb:

aaacaa b ba

Critical pair: aaacaaaacaccaccacb=caacaa.

Reduce LHS:

[21]aaaca(aaacaccac)cacb
[13]⇒ aaacac(aaacacb)
⇒ aaacac

Defines rule #2.

Referenced by [25], [26].

[25] acaacaab=caacac

Overlap of [23] aaacaab=caaca with [11] bc=caccacb:

aaacaa b bc

Critical pair: aaacaacaccacb=caacac.

Reduce LHS:

[18]aaa(caacaccacb)
[24]⇒ a(aaacac)b
⇒ acaacaab

Referenced by [27].

[26] caacaab=1

Overlap of [13] aaacacb=1 with [24] aaacac=caacaa:

aaacacb aaacac

Critical pair: caacaab=1.

Defines rule #3.

Referenced by [27].

[27] caacac=a

Overlap of [25] acaacaab=caacac with [26] caacaab=1:

a caacaab caacaab

Critical pair: a=caacac.

Flip LHS and RHS.

Defines rule #1.