Certificate for #3107 ⟨a, b | aabbaabaabb=1⟩

Back:⟨a, b | aabbaabaabb=1⟩

Completion settings:

[1] aabbaabaabb=1

Axiom: aabbaabaabb=1.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #6.

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

[3] d=bbcbcbb

Axiom: bbaabaabb=d.

Reduce LHS:

[2]bb(aa)baabb
[2]⇒ bbcb(aa)bb
⇒ bbcbcbb

Flip LHS and RHS.

Referenced by [7].

[4] cbbcbcbb=1

Overlap of [1] aabbaabaabb=1 with [2] aa=c:

aabbaabaabb aa

Critical pair: cbbaabaabb=1.

Reduce LHS:

[2]cbb(aa)baabb
[2]⇒ cbbcb(aa)bb
⇒ cbbcbcbb

Referenced by [6], [8].

[5] ca=ac

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

a a aa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16].

[6] cbcbb=cbbcb

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

cbbcb cbb cbbcbcbb

Critical pair: cbbcb=cbcbb.

Flip LHS and RHS.

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

[7] d=bbcbbcb

Simplify [3] d=bbcbcbb.

Reduce RHS:

[6]bb(cbcbb)
⇒ bbcbbcb

Referenced by [10].

[8] cbbcbbcb=1

Overlap of [4] cbbcbcbb=1 with [6] cbcbb=cbbcb:

cbb cbcbb cbcbb

Critical pair: cbbcbbcb=1.

Referenced by [9], [11].

[9] cbb=bcb

Overlap of [8] cbbcbbcb=1 with [6] cbcbb=cbbcb:

cbbcbb cb cbcbb

Critical pair: cbbcbbcbbcb=cbb.

Reduce LHS:

[8](cbbcbbcb)bcb
⇒ bcb

Flip LHS and RHS.

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

[10] d=bbbcbcb

Simplify [7] d=bbcbbcb.

Reduce RHS:

[9]bb(cbb)cb
⇒ bbbcbcb

Referenced by [14].

[11] bbcbcbcb=1

Overlap of [8] cbbcbbcb=1 with [9] cbb=bcb:

cbbcbbcb cbb

Critical pair: bcbcbbcb=1.

Reduce LHS:

[9]bcb(cbb)cb
[9]⇒ b(cbb)cbcb
⇒ bbcbcbcb

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

[12] bcbcbcbcb=c

Overlap of [9] cbb=bcb with [11] bbcbcbcb=1:

c bb bbcbcbcb

Critical pair: c=bcbcbcbcb.

Flip LHS and RHS.

Referenced by [13].

[13] cb=bc

Overlap of [11] bbcbcbcb=1 with [12] bcbcbcbcb=c:

b bcbcbcb bcbcbcbcb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [14], [15], [17], [18], [19], [20], [21].

[14] d=bbbbbcc

Simplify [10] d=bbbcbcb.

Reduce RHS:

[13]bbb(cb)cb
[13]⇒ bbbbc(cb)
[13]⇒ bbbb(cb)c
⇒ bbbbbcc

Defines rule #5.

[15] bbbbbccc=1

Overlap of [11] bbcbcbcb=1 with [13] cb=bc:

bb cbcbcb cb

Critical pair: bbbccbcb=1.

Reduce LHS:

[13]bbbc(cb)cb
[13]⇒ bbb(cb)ccb
[13]⇒ bbbbcc(cb)
[13]⇒ bbbbc(cb)c
[13]⇒ bbbb(cb)cc
⇒ bbbbbccc

Defines rule #2.

Referenced by [16], [21].

[16] bbbbbaccc=a

Overlap of [15] bbbbbccc=1 with [5] ca=ac:

bbbbbcc c ca

Critical pair: bbbbbccac=a.

Reduce LHS:

[5]bbbbbc(ca)c
[5]⇒ bbbbb(ca)cc
⇒ bbbbbaccc

Referenced by [17].

[17] bbbbbabccc=ab

Overlap of [16] bbbbbaccc=a with [13] cb=bc:

bbbbbacc c cb

Critical pair: bbbbbaccbc=ab.

Reduce LHS:

[13]bbbbbac(cb)c
[13]⇒ bbbbba(cb)cc
⇒ bbbbbabccc

Referenced by [18].

[18] bbbbbabbccc=abb

Overlap of [17] bbbbbabccc=ab with [13] cb=bc:

bbbbbabcc c cb

Critical pair: bbbbbabccbc=abb.

Reduce LHS:

[13]bbbbbabc(cb)c
[13]⇒ bbbbbab(cb)cc
⇒ bbbbbabbccc

Referenced by [19].

[19] bbbbbabbbccc=abbb

Overlap of [18] bbbbbabbccc=abb with [13] cb=bc:

bbbbbabbcc c cb

Critical pair: bbbbbabbccbc=abbb.

Reduce LHS:

[13]bbbbbabbc(cb)c
[13]⇒ bbbbbabb(cb)cc
⇒ bbbbbabbbccc

Referenced by [20].

[20] bbbbbabbbbccc=abbbb

Overlap of [19] bbbbbabbbccc=abbb with [13] cb=bc:

bbbbbabbbcc c cb

Critical pair: bbbbbabbbccbc=abbbb.

Reduce LHS:

[13]bbbbbabbbc(cb)c
[13]⇒ bbbbbabbb(cb)cc
⇒ bbbbbabbbbccc

Referenced by [21].

[21] bbbbba=abbbbb

Overlap of [20] bbbbbabbbbccc=abbbb with [13] cb=bc:

bbbbbabbbbcc c cb

Critical pair: bbbbbabbbbccbc=abbbbb.

Reduce LHS:

[13]bbbbbabbbbc(cb)c
[13]⇒ bbbbbabbbb(cb)cc
[15]⇒ bbbbba(bbbbbccc)
⇒ bbbbba

Defines rule #4.