Certificate for #2982 ⟨a, b | aaabbbaaabb=1⟩

Back:⟨a, b | aaabbbaaabb=1⟩

Completion settings:

[1] aaabbbaaabb=1

Axiom: aaabbbaaabb=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #6.

Referenced by [3], [4], [5].

[3] d=bbbcbb

Axiom: bbbaaabb=d.

Reduce LHS:

[2]bbb(aaa)bb
⇒ bbbcbb

Flip LHS and RHS.

Referenced by [9].

[4] cbbbcbb=1

Overlap of [1] aaabbbaaabb=1 with [2] aaa=c:

aaabbbaaabb aaa

Critical pair: cbbbaaabb=1.

Reduce LHS:

[2]cbbb(aaa)bb
⇒ cbbbcbb

Referenced by [6], [7].

[5] ca=ac

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

a aa aaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [15].

[6] cbbb=bcbb

Overlap of [4] cbbbcbb=1 with [4] cbbbcbb=1:

cbbb cbb cbbbcbb

Critical pair: cbbb=bcbb.

Referenced by [7].

[7] bcbbcbb=1

Overlap of [4] cbbbcbb=1 with [6] cbbb=bcbb:

cbbbcbb cbbb

Critical pair: bcbbcbb=1.

Referenced by [8], [10].

[8] cbb=bcb

Overlap of [7] bcbbcbb=1 with [7] bcbbcbb=1:

bcb bcbb bcbbcbb

Critical pair: bcb=cbb.

Flip LHS and RHS.

Referenced by [9], [10], [11].

[9] d=bbbbcb

Simplify [3] d=bbbcbb.

Reduce RHS:

[8]bbb(cbb)
⇒ bbbbcb

Referenced by [13].

[10] bbbcbcb=1

Overlap of [7] bcbbcbb=1 with [8] cbb=bcb:

b cbbcbb cbb

Critical pair: bbcbcbb=1.

Reduce LHS:

[8]bbcb(cbb)
[8]⇒ bb(cbb)cb
⇒ bbbcbcb

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

[11] bbcbcbcb=c

Overlap of [8] cbb=bcb with [10] bbbcbcb=1:

c bb bbbcbcb

Critical pair: c=bcbbcbcb.

Reduce RHS:

[8]b(cbb)cbcb
⇒ bbcbcbcb

Flip LHS and RHS.

Referenced by [12].

[12] cb=bc

Overlap of [10] bbbcbcb=1 with [11] bbcbcbcb=c:

b bbcbcb bbcbcbcb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #1.

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

[13] d=bbbbbc

Simplify [9] d=bbbbcb.

Reduce RHS:

[12]bbbb(cb)
⇒ bbbbbc

Defines rule #5.

[14] bbbbbcc=1

Overlap of [10] bbbcbcb=1 with [12] cb=bc:

bbb cbcb cb

Critical pair: bbbbccb=1.

Reduce LHS:

[12]bbbbc(cb)
[12]⇒ bbbb(cb)c
⇒ bbbbbcc

Defines rule #2.

Referenced by [15], [20].

[15] bbbbbacc=a

Overlap of [14] bbbbbcc=1 with [5] ca=ac:

bbbbbc c ca

Critical pair: bbbbbcac=a.

Reduce LHS:

[5]bbbbb(ca)c
⇒ bbbbbacc

Referenced by [16].

[16] bbbbbabcc=ab

Overlap of [15] bbbbbacc=a with [12] cb=bc:

bbbbbac c cb

Critical pair: bbbbbacbc=ab.

Reduce LHS:

[12]bbbbba(cb)c
⇒ bbbbbabcc

Referenced by [17].

[17] bbbbbabbcc=abb

Overlap of [16] bbbbbabcc=ab with [12] cb=bc:

bbbbbabc c cb

Critical pair: bbbbbabcbc=abb.

Reduce LHS:

[12]bbbbbab(cb)c
⇒ bbbbbabbcc

Referenced by [18].

[18] bbbbbabbbcc=abbb

Overlap of [17] bbbbbabbcc=abb with [12] cb=bc:

bbbbbabbc c cb

Critical pair: bbbbbabbcbc=abbb.

Reduce LHS:

[12]bbbbbabb(cb)c
⇒ bbbbbabbbcc

Referenced by [19].

[19] bbbbbabbbbcc=abbbb

Overlap of [18] bbbbbabbbcc=abbb with [12] cb=bc:

bbbbbabbbc c cb

Critical pair: bbbbbabbbcbc=abbbb.

Reduce LHS:

[12]bbbbbabbb(cb)c
⇒ bbbbbabbbbcc

Referenced by [20].

[20] bbbbba=abbbbb

Overlap of [19] bbbbbabbbbcc=abbbb with [12] cb=bc:

bbbbbabbbbc c cb

Critical pair: bbbbbabbbbcbc=abbbbb.

Reduce LHS:

[12]bbbbbabbbb(cb)c
[14]⇒ bbbbba(bbbbbcc)
⇒ bbbbba

Defines rule #4.