Certificate for #14 ⟨a, b | abba=1⟩

Back:⟨a, b | abba=1⟩

Completion settings:

[1] abba=1

Axiom: abba=1.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #1.

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

[3] bb=d

Axiom: bb=d.

Defines rule #2.

Referenced by [4], [6].

[4] ada=1

Overlap of [1] abba=1 with [3] bb=d:

a bba bb

Critical pair: ada=1.

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

[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 [10].

[6] db=bd

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

b b bb

Critical pair: bd=db.

Flip LHS and RHS.

Defines rule #7.

Referenced by [12].

[7] cda=a

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

a a ada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [10].

[8] da=ad

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

ad a ada

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #6.

Referenced by [9], [10].

[9] dc=1

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

d a aa

Critical pair: dc=ada.

Reduce RHS:

[4](ada)
⇒ 1

Defines rule #8.

Referenced by [13].

[10] acd=a

Simplify [7] cda=a.

Reduce LHS:

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

Referenced by [11].

[11] cd=1

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

ad a acd

Critical pair: ada=cd.

Reduce LHS:

[4](ada)
⇒ 1

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

[12] cbd=b

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

c d db

Critical pair: cbd=b.

Referenced by [13].

[13] cb=bc

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

cb d dc

Critical pair: cb=bc.

Defines rule #4.