Certificate for #26 ⟨a, b | aaa=1, abb=1⟩

Back:⟨a, b | aaa=1, abb=1⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

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

[2] abb=1

Axiom: abb=1.

Referenced by [3].

[3] aa=bb

Overlap of [1] aaa=1 with [2] abb=1:

aa a abb

Critical pair: aa=bb.

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

[4] bba=1

Overlap of [1] aaa=1 with [3] aa=bb:

aaa aa

Critical pair: bba=1.

Referenced by [6].

[5] a=bbbb

Overlap of [1] aaa=1 with [3] aa=bb:

aa a aa

Critical pair: aabb=a.

Reduce LHS:

[3](aa)bb
⇒ bbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] bbbbbb=1

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

a a aa

Critical pair: abb=bba.

Reduce LHS:

[5](a)bb
⇒ bbbbbb

Reduce RHS:

[4](bba)
⇒ 1

Defines rule #1.