Certificate for #2914 ⟨a, b | aaabaabaaba=1⟩

Back:⟨a, b | aaabaabaaba=1⟩

Completion settings:

[1] aaabaabaaba=1

Axiom: aaabaabaaba=1.

Referenced by [4].

[2] aaaa=c

Axiom: aaaa=c.

Defines rule #7.

Referenced by [5], [6], [7], [18], [20], [32].

[3] baabaab=d

Axiom: baabaab=d.

Referenced by [4], [10], [19], [26].

[4] aaada=1

Overlap of [1] aaabaabaaba=1 with [3] baabaab=d:

aaa baabaaba baabaab

Critical pair: aaada=1.

Referenced by [6], [7], [8], [9], [12], [13].

[5] ca=ac

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

a aaa aaaa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [15], [32], [34], [35].

[6] cda=a

Overlap of [2] aaaa=c with [4] aaada=1:

a aaa aaada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [11].

[7] aaadc=aaa

Overlap of [4] aaada=1 with [2] aaaa=c:

aaad a aaaa

Critical pair: aaadc=aaa.

Referenced by [12].

[8] aada=aaad

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

aaad a aaada

Critical pair: aaad=aada.

Flip LHS and RHS.

Referenced by [17], [18], [20], [21].

[9] cd=1

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

cd a aaada

Critical pair: cd=aaada.

Reduce RHS:

[4](aaada)
⇒ 1

Referenced by [16], [18], [20], [23], [24], [26], [27], [29].

[10] daab=baad

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

baa baab baabaab

Critical pair: baad=daab.

Flip LHS and RHS.

Referenced by [11], [20].

[11] cbaad=aab

Overlap of [6] cda=a with [10] daab=baad:

c da daab

Critical pair: cbaad=aab.

Referenced by [14].

[12] aadc=aa

Overlap of [4] aaada=1 with [7] aaadc=aaa:

aaad a aaadc

Critical pair: aaadaaa=aadc.

Reduce LHS:

[4](aaada)aa
⇒ aa

Flip LHS and RHS.

Referenced by [13], [14].

[13] adc=a

Overlap of [4] aaada=1 with [12] aadc=aa:

aaad a aadc

Critical pair: aaadaa=adc.

Reduce LHS:

[4](aaada)a
⇒ a

Flip LHS and RHS.

Referenced by [15].

[14] cbaa=aabc

Overlap of [11] cbaad=aab with [12] aadc=aa:

cb aad aadc

Critical pair: cbaa=aabc.

Referenced by [18], [22], [25].

[15] adac=aa

Overlap of [13] adc=a with [5] ca=ac:

ad c ca

Critical pair: adac=aa.

Referenced by [16], [18].

[16] ada=aad

Overlap of [15] adac=aa with [9] cd=1:

ada c cd

Critical pair: ada=aad.

Referenced by [17], [18], [21].

[17] aadda=aaadd

Overlap of [16] ada=aad with [16] ada=aad:

ad a ada

Critical pair: adaad=aadda.

Reduce LHS:

[16](ada)ad
[8]⇒ (aada)d
⇒ aaadd

Flip LHS and RHS.

Referenced by [30].

[18] aabaa=bc

Overlap of [15] adac=aa with [14] cbaa=aabc:

ada c cbaa

Critical pair: adaaabc=aabaa.

Reduce LHS:

[16](ada)aabc
[8]⇒ (aada)abc
[8]⇒ a(aada)bc
[2]⇒ (aaaa)dbc
[9]⇒ (cd)bc
⇒ bc

Flip LHS and RHS.

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

[19] daa=baabbc

Overlap of [3] baabaab=d with [18] aabaa=bc:

baab aab aabaa

Critical pair: baabbc=daa.

Flip LHS and RHS.

Referenced by [25].

[20] dbc=b

Overlap of [10] daab=baad with [18] aabaa=bc:

d aab aabaa

Critical pair: dbc=baadaa.

Reduce RHS:

[8]b(aada)a
[8]⇒ ba(aada)
[2]⇒ b(aaaa)d
[9]⇒ b(cd)
⇒ b

Referenced by [21], [23], [24], [25], [28].

[21] aaadbaa=ab

Overlap of [16] ada=aad with [18] aabaa=bc:

ad a aabaa

Critical pair: adbc=aadabaa.

Reduce LHS:

[20]a(dbc)
⇒ ab

Reduce RHS:

[8](aada)baa
⇒ aaadbaa

Flip LHS and RHS.

Referenced by [32].

[22] baabc=aabbc

Overlap of [18] aabaa=bc with [18] aabaa=bc:

aab aa aabaa

Critical pair: aabbc=bcbaa.

Reduce RHS:

[14]b(cbaa)
⇒ baabc

Flip LHS and RHS.

Referenced by [25].

[23] cb=bc

Overlap of [9] cd=1 with [20] dbc=b:

c d dbc

Critical pair: cb=bc.

Defines rule #1.

Referenced by [25], [27], [28], [29], [30], [31], [32], [36], [37], [38].

[24] bd=db

Overlap of [20] dbc=b with [9] cd=1:

db c cd

Critical pair: db=bd.

Flip LHS and RHS.

Referenced by [26].

[25] bbaa=baabbbbcc

Overlap of [20] dbc=b with [14] cbaa=aabc:

db c cbaa

Critical pair: dbaabc=bbaa.

Reduce LHS:

[22]d(baabc)
[19]⇒ (daa)bbc
[23]⇒ baabb(cb)bc
[23]⇒ baabbb(cb)c
⇒ baabbbbcc

Flip LHS and RHS.

Referenced by [32], [33].

[26] dd=bbb

Overlap of [3] baabaab=d with [24] bd=db:

baabaa b bd

Critical pair: baabaadb=dd.

Reduce LHS:

[18]b(aabaa)db
[9]⇒ bb(cd)b
⇒ bbb

Flip LHS and RHS.

Referenced by [27].

[27] d=bbbc

Overlap of [9] cd=1 with [26] dd=bbb:

c d dd

Critical pair: cbbb=d.

Reduce LHS:

[23](cb)bb
[23]⇒ b(cb)b
[23]⇒ bb(cb)
⇒ bbbc

Flip LHS and RHS.

Defines rule #5.

Referenced by [28], [29], [30], [31], [32].

[28] bbbbcc=b

Overlap of [20] dbc=b with [27] d=bbbc:

dbc d

Critical pair: bbbcbc=b.

Reduce LHS:

[23]bbb(cb)c
⇒ bbbbcc

Referenced by [30], [31], [32], [33].

[29] bbbcc=1

Overlap of [9] cd=1 with [27] d=bbbc:

c d d

Critical pair: cbbbc=1.

Reduce LHS:

[23](cb)bbc
[23]⇒ b(cb)bc
[23]⇒ bb(cb)c
⇒ bbbcc

Defines rule #2.

Referenced by [34], [37], [38].

[30] aadda=aaabbb

Simplify [17] aadda=aaadd.

Reduce RHS:

[27]aaa(d)d
[27]⇒ aaabbbc(d)
[23]⇒ aaabbb(cb)bbc
[23]⇒ aaabbbb(cb)bc
[23]⇒ aaabbbbb(cb)c
[28]⇒ aaabb(bbbbcc)
⇒ aaabbb

Referenced by [31].

[31] aabbba=aaabbb

Overlap of [30] aadda=aaabbb with [27] d=bbbc:

aa dda d

Critical pair: aabbbcda=aaabbb.

Reduce LHS:

[27]aabbbc(d)a
[23]⇒ aabbb(cb)bbca
[23]⇒ aabbbb(cb)bca
[23]⇒ aabbbbb(cb)ca
[28]⇒ aabb(bbbbcc)a
⇒ aabbba

Referenced by [32].

[32] bbbabcc=ab

Overlap of [21] aaadbaa=ab with [27] d=bbbc:

aaa dbaa d

Critical pair: aaabbbcbaa=ab.

Reduce LHS:

[23]aaabbb(cb)aa
[5]⇒ aaabbbb(ca)a
[5]⇒ aaabbbba(ca)
[25]⇒ aaabb(bbaa)c
[31]⇒ a(aabbba)abbbbccc
[2]⇒ (aaaa)bbbabbbbccc
[23]⇒ (cb)bbabbbbccc
[23]⇒ b(cb)babbbbccc
[23]⇒ bb(cb)abbbbccc
[5]⇒ bbb(ca)bbbbccc
[23]⇒ bbba(cb)bbbccc
[23]⇒ bbbab(cb)bbccc
[23]⇒ bbbabb(cb)bccc
[23]⇒ bbbabbb(cb)ccc
[28]⇒ bbba(bbbbcc)cc
⇒ bbbabcc

Referenced by [36].

[33] bbaa=baab

Simplify [25] bbaa=baabbbbcc.

Reduce RHS:

[28]baa(bbbbcc)
⇒ baab

Referenced by [35].

[34] bbbacc=a

Overlap of [29] bbbcc=1 with [5] ca=ac:

bbbc c ca

Critical pair: bbbcac=a.

Reduce LHS:

[5]bbb(ca)c
⇒ bbbacc

Referenced by [35].

[35] baabbcc=aa

Overlap of [34] bbbacc=a with [5] ca=ac:

bbbac c ca

Critical pair: bbbacac=aa.

Reduce LHS:

[5]bbba(ca)c
[33]⇒ b(bbaa)cc
[33]⇒ (bbaa)bcc
⇒ baabbcc

Referenced by [37].

[36] bbbabbcc=abb

Overlap of [32] bbbabcc=ab with [23] cb=bc:

bbbabc c cb

Critical pair: bbbabcbc=abb.

Reduce LHS:

[23]bbbab(cb)c
⇒ bbbabbcc

Referenced by [38].

[37] baa=aab

Overlap of [35] baabbcc=aa with [23] cb=bc:

baabbc c cb

Critical pair: baabbcbc=aab.

Reduce LHS:

[23]baabb(cb)c
[29]⇒ baa(bbbcc)
⇒ baa

Defines rule #6.

[38] bbba=abbb

Overlap of [36] bbbabbcc=abb with [23] cb=bc:

bbbabbc c cb

Critical pair: bbbabbcbc=abbb.

Reduce LHS:

[23]bbbabb(cb)c
[29]⇒ bbba(bbbcc)
⇒ bbba

Defines rule #4.