Certificate for #724 ⟨a, b | abbaabbba=1⟩

Back:⟨a, b | abbaabbba=1⟩

Completion settings:

[1] abbaabbba=1

Axiom: abbaabbba=1.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #6.

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

[3] d=bbbcbb

Axiom: bbbaabb=d.

Reduce LHS:

[2]bbb(aa)bb
⇒ bbbcbb

Flip LHS and RHS.

Referenced by [15].

[4] abbcbbba=1

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

abb aabbba aa

Critical pair: abbcbbba=1.

Referenced by [6], [7], [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 [17].

[6] abbcbbbc=a

Overlap of [4] abbcbbba=1 with [2] aa=c:

abbcbbb a aa

Critical pair: abbcbbbc=a.

Referenced by [8], [9].

[7] bbcbbba=abbcbbb

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

abbcbbb a abbcbbba

Critical pair: abbcbbb=bbcbbba.

Flip LHS and RHS.

Referenced by [16].

[8] bbcbbbc=1

Overlap of [4] abbcbbba=1 with [6] abbcbbbc=a:

abbcbbb a abbcbbbc

Critical pair: abbcbbba=bbcbbbc.

Reduce LHS:

[4](abbcbbba)
⇒ 1

Flip LHS and RHS.

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

[9] abbcb=abbbc

Overlap of [6] abbcbbbc=a with [8] bbcbbbc=1:

abbcb bbc bbcbbbc

Critical pair: abbcb=abbbc.

Referenced by [16].

[10] bbcb=bbbc

Overlap of [8] bbcbbbc=1 with [8] bbcbbbc=1:

bbcb bbc bbcbbbc

Critical pair: bbcb=bbbc.

Referenced by [11], [12], [13], [15], [16], [17].

[11] bbbbbcc=1

Overlap of [8] bbcbbbc=1 with [10] bbcb=bbbc:

bbcbbbc bbcb

Critical pair: bbbcbbc=1.

Reduce LHS:

[10]b(bbcb)bc
[10]⇒ bb(bbcb)c
⇒ bbbbbcc

Defines rule #2.

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

[12] bbbbccb=1

Overlap of [10] bbcb=bbbc with [10] bbcb=bbbc:

bbc b bbcb

Critical pair: bbcbbbc=bbbcbcb.

Reduce LHS:

[10](bbcb)bbc
[10]⇒ b(bbcb)bc
[10]⇒ bb(bbcb)c
[11]⇒ (bbbbbcc)
⇒ 1

Reduce RHS:

[10]b(bbcb)cb
⇒ bbbbccb

Flip LHS and RHS.

Referenced by [13], [14].

[13] bcb=bbc

Overlap of [10] bbcb=bbbc with [12] bbbbccb=1:

bbc b bbbbccb

Critical pair: bbc=bbbcbbbccb.

Reduce RHS:

[10]b(bbcb)bbccb
[10]⇒ bb(bbcb)bccb
[10]⇒ bbb(bbcb)ccb
[11]⇒ b(bbbbbcc)cb
⇒ bcb

Flip LHS and RHS.

Referenced by [14].

[14] cb=bc

Overlap of [12] bbbbccb=1 with [13] bcb=bbc:

bbbbcc b bcb

Critical pair: bbbbccbbc=cb.

Reduce LHS:

[12](bbbbccb)bc
⇒ bc

Flip LHS and RHS.

Defines rule #1.

Referenced by [18], [19], [20], [21], [22].

[15] d=bbbbbc

Simplify [3] d=bbbcbb.

Reduce RHS:

[10]b(bbcb)b
[10]⇒ bb(bbcb)
⇒ bbbbbc

Defines rule #5.

[16] bbcbbba=abbbbbc

Simplify [7] bbcbbba=abbcbbb.

Reduce RHS:

[9](abbcb)bb
[10]⇒ ab(bbcb)b
[10]⇒ abb(bbcb)
⇒ abbbbbc

Referenced by [17].

[17] bbbbbac=abbbbbc

Overlap of [16] bbcbbba=abbbbbc with [10] bbcb=bbbc:

bbcbbba bbcb

Critical pair: bbbcbba=abbbbbc.

Reduce LHS:

[10]b(bbcb)ba
[10]⇒ bb(bbcb)a
[5]⇒ bbbbb(ca)
⇒ bbbbbac

Referenced by [18].

[18] bbbbbabc=abbbbbbc

Overlap of [17] bbbbbac=abbbbbc with [14] cb=bc:

bbbbba c cb

Critical pair: bbbbbabc=abbbbbcb.

Reduce RHS:

[14]abbbbb(cb)
⇒ abbbbbbc

Referenced by [19].

[19] bbbbbabbc=abbbbbbbc

Overlap of [18] bbbbbabc=abbbbbbc with [14] cb=bc:

bbbbbab c cb

Critical pair: bbbbbabbc=abbbbbbcb.

Reduce RHS:

[14]abbbbbb(cb)
⇒ abbbbbbbc

Referenced by [20].

[20] bbbbbabbbc=abbbbbbbbc

Overlap of [19] bbbbbabbc=abbbbbbbc with [14] cb=bc:

bbbbbabb c cb

Critical pair: bbbbbabbbc=abbbbbbbcb.

Reduce RHS:

[14]abbbbbbb(cb)
⇒ abbbbbbbbc

Referenced by [21].

[21] bbbbbabbbbc=abbbbbbbbbc

Overlap of [20] bbbbbabbbc=abbbbbbbbc with [14] cb=bc:

bbbbbabbb c cb

Critical pair: bbbbbabbbbc=abbbbbbbbcb.

Reduce RHS:

[14]abbbbbbbb(cb)
⇒ abbbbbbbbbc

Referenced by [22].

[22] bbbbbabbbbbc=abbbbbbbbbbc

Overlap of [21] bbbbbabbbbc=abbbbbbbbbc with [14] cb=bc:

bbbbbabbbb c cb

Critical pair: bbbbbabbbbbc=abbbbbbbbbcb.

Reduce RHS:

[14]abbbbbbbbb(cb)
⇒ abbbbbbbbbbc

Referenced by [23].

[23] bbbbba=abbbbb

Overlap of [22] bbbbbabbbbbc=abbbbbbbbbbc with [11] bbbbbcc=1:

bbbbba bbbbbc bbbbbcc

Critical pair: bbbbba=abbbbbbbbbbcc.

Reduce RHS:

[11]abbbbb(bbbbbcc)
⇒ abbbbb

Defines rule #4.