Certificate for #10016 ⟨a, b | aa=1, abbabb=bb⟩

Back:⟨a, b | aa=1, abbabb=bb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #2.

Referenced by [7], [8].

[2] abbabb=bb

Axiom: abbabb=bb.

Referenced by [4].

[3] abb=c

Axiom: abb=c.

Referenced by [4], [5].

[4] bb=cc

Overlap of [2] abbabb=bb with [3] abb=c:

abbabb abb

Critical pair: cabb=bb.

Reduce LHS:

[3]c(abb)
⇒ cc

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] acc=c

Overlap of [3] abb=c with [4] bb=cc:

a bb bb

Critical pair: acc=c.

Referenced by [7], [10].

[6] bcc=ccb

Overlap of [4] bb=cc with [4] bb=cc:

b b bb

Critical pair: bcc=ccb.

Defines rule #6.

Referenced by [9].

[7] ac=cc

Overlap of [1] aa=1 with [5] acc=c:

a a acc

Critical pair: ac=cc.

Defines rule #1.

Referenced by [8].

[8] ccc=c

Overlap of [1] aa=1 with [7] ac=cc:

a a ac

Critical pair: acc=c.

Reduce LHS:

[7](ac)c
⇒ ccc

Defines rule #4.

Referenced by [9].

[9] ccbc=bc

Overlap of [6] bcc=ccb with [8] ccc=c:

b cc ccc

Critical pair: bc=ccbc.

Flip LHS and RHS.

Defines rule #7.

Referenced by [10].

[10] abc=cbc

Overlap of [5] acc=c with [9] ccbc=bc:

a cc ccbc

Critical pair: abc=cbc.

Defines rule #5.