Certificate for #3304 ⟨a, b | abbbbbbbbba=1⟩

Back:⟨a, b | abbbbbbbbba=1⟩

Completion settings:

[1] abbbbbbbbba=1

Axiom: abbbbbbbbba=1.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #1.

Referenced by [5], [6], [8].

[3] bbbbbbbbb=d

Axiom: bbbbbbbbb=d.

Defines rule #8.

Referenced by [4], [11].

[4] ada=1

Overlap of [1] abbbbbbbbba=1 with [3] bbbbbbbbb=d:

a bbbbbbbbba bbbbbbbbb

Critical pair: ada=1.

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

[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 #2.

Referenced by [9].

[6] cda=a

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

a a ada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9].

[7] da=ad

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

ad a ada

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #5.

Referenced by [8], [9].

[8] dc=1

Overlap of [7] da=ad with [2] aa=c:

d a aa

Critical pair: dc=ada.

Reduce RHS:

[4](ada)
⇒ 1

Defines rule #7.

Referenced by [13].

[9] acd=a

Simplify [6] cda=a.

Reduce LHS:

[7]c(da)
[5]⇒ (ca)d
⇒ acd

Referenced by [10].

[10] cd=1

Overlap of [4] ada=1 with [9] acd=a:

ad a acd

Critical pair: ada=cd.

Reduce LHS:

[4](ada)
⇒ 1

Flip LHS and RHS.

Defines rule #4.

Referenced by [12].

[11] db=bd

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

b bbbbbbbb bbbbbbbbb

Critical pair: bd=db.

Flip LHS and RHS.

Defines rule #6.

Referenced by [12].

[12] cbd=b

Overlap of [10] cd=1 with [11] db=bd:

c d db

Critical pair: cbd=b.

Referenced by [13].

[13] cb=bc

Overlap of [12] cbd=b with [8] dc=1:

cb d dc

Critical pair: cb=bc.

Defines rule #3.