Certificate for #317 ⟨a, b | aabbbaba=1⟩

Back:⟨a, b | aabbbaba=1⟩

Completion settings:

[1] aabbbaba=1

Axiom: aabbbaba=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [15], [17], [20].

[3] bbbab=d

Axiom: bbbab=d.

Defines rule #14.

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

[4] aada=1

Overlap of [1] aabbbaba=1 with [3] bbbab=d:

aa bbbaba bbbab

Critical pair: aada=1.

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

[5] ac=ca

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

a aa aaa

Critical pair: ac=ca.

Defines rule #3.

Referenced by [16], [23].

[6] cda=a

Overlap of [2] aaa=c with [4] aada=1:

a aa aada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

[7] aad=ada

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

aad a aada

Critical pair: aad=ada.

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

[8] adaa=cd

Overlap of [6] cda=a with [4] aada=1:

cd a aada

Critical pair: cd=aada.

Reduce RHS:

[7](aad)a
⇒ adaa

Flip LHS and RHS.

Referenced by [9], [10].

[9] cd=1

Overlap of [4] aada=1 with [7] aad=ada:

aada aad

Critical pair: adaa=1.

Reduce LHS:

[8](adaa)
⇒ cd

Defines rule #1.

Referenced by [10], [11], [13], [17], [21], [24].

[10] ad=da

Overlap of [4] aada=1 with [7] aad=ada:

aad a aad

Critical pair: aadada=ad.

Reduce LHS:

[7](aad)ada
[8]⇒ (adaa)da
[9]⇒ (cd)da
⇒ da

Flip LHS and RHS.

Defines rule #4.

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

[11] dc=1

Overlap of [2] aaa=c with [10] ad=da:

aa a ad

Critical pair: aada=cd.

Reduce LHS:

[7](aad)a
[10]⇒ (ad)aa
[2]⇒ d(aaa)
⇒ dc

Reduce RHS:

[9](cd)
⇒ 1

Defines rule #2.

Referenced by [15], [26].

[12] dbbab=bbbda

Overlap of [3] bbbab=d with [3] bbbab=d:

bbba b bbbab

Critical pair: bbbad=dbbab.

Reduce LHS:

[10]bbb(ad)
⇒ bbbda

Flip LHS and RHS.

Defines rule #9.

Referenced by [13], [14].

[13] cbbbda=bbab

Overlap of [9] cd=1 with [12] dbbab=bbbda:

c d dbbab

Critical pair: cbbbda=bbab.

Referenced by [15].

[14] dabbab=abbbda

Overlap of [10] ad=da with [12] dbbab=bbbda:

a d dbbab

Critical pair: abbbda=dabbab.

Flip LHS and RHS.

Defines rule #11.

[15] cbbb=bbabaa

Overlap of [13] cbbbda=bbab with [2] aaa=c:

cbbbd a aaa

Critical pair: cbbbdc=bbabaa.

Reduce LHS:

[11]cbbb(dc)
⇒ cbbb

Defines rule #8.

Referenced by [16], [17].

[16] cabbb=abbabaa

Overlap of [5] ac=ca with [15] cbbb=bbabaa:

a c cbbb

Critical pair: abbabaa=cabbb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [23].

[17] bbabcb=1

Overlap of [15] cbbb=bbabaa with [3] bbbab=d:

c bbb bbbab

Critical pair: cd=bbabaaab.

Reduce LHS:

[9](cd)
⇒ 1

Reduce RHS:

[2]bbab(aaa)b
⇒ bbabcb

Flip LHS and RHS.

Referenced by [18], [19].

[18] babcb=bbabc

Overlap of [17] bbabcb=1 with [17] bbabcb=1:

bbabc b bbabcb

Critical pair: bbabc=babcb.

Flip LHS and RHS.

Referenced by [19], [22].

[19] abcb=babc

Overlap of [17] bbabcb=1 with [18] babcb=bbabc:

bbabc b babcb

Critical pair: bbabcbbabc=abcb.

Reduce LHS:

[17](bbabcb)babc
⇒ babc

Flip LHS and RHS.

Defines rule #6.

Referenced by [20].

[20] aababc=cbcb

Overlap of [2] aaa=c with [19] abcb=babc:

aa a abcb

Critical pair: aababc=cbcb.

Referenced by [21], [22].

[21] aabab=cbcbd

Overlap of [20] aababc=cbcb with [9] cd=1:

aabab c cd

Critical pair: aabab=cbcbd.

Defines rule #7.

[22] aabbabc=cbcbb

Overlap of [20] aababc=cbcb with [18] babcb=bbabc:

aa babc babcb

Critical pair: aabbabc=cbcbb.

Referenced by [24].

[23] caabbb=aabbabaa

Overlap of [5] ac=ca with [16] cabbb=abbabaa:

a c cabbb

Critical pair: aabbabaa=caabbb.

Flip LHS and RHS.

Referenced by [25].

[24] aabbab=cbcbbd

Overlap of [22] aabbabc=cbcbb with [9] cd=1:

aabbab c cd

Critical pair: aabbab=cbcbbd.

Defines rule #13.

Referenced by [25].

[25] caabbb=cbcbbdaa

Simplify [23] caabbb=aabbabaa.

Reduce RHS:

[24](aabbab)aa
⇒ cbcbbdaa

Referenced by [26].

[26] aabbb=bcbbdaa

Overlap of [11] dc=1 with [25] caabbb=cbcbbdaa:

d c caabbb

Critical pair: dcbcbbdaa=aabbb.

Reduce LHS:

[11](dc)bcbbdaa
⇒ bcbbdaa

Flip LHS and RHS.

Defines rule #12.