Certificate for #1487 ⟨a, b, c | ab=1, acc=bb⟩

Back:⟨a, b, c | ab=1, acc=bb⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Referenced by [3], [5].

[2] bb=acc

Axiom: acc=bb.

Flip LHS and RHS.

Referenced by [3], [4].

[3] b=aacc

Overlap of [1] ab=1 with [2] bb=acc:

a b bb

Critical pair: aacc=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] accaacc=aaccacc

Overlap of [2] bb=acc with [2] bb=acc:

b b bb

Critical pair: bacc=accb.

Reduce LHS:

[3](b)acc
⇒ aaccacc

Reduce RHS:

[3]acc(b)
⇒ accaacc

Flip LHS and RHS.

Defines rule #2.

[5] aaacc=1

Overlap of [1] ab=1 with [3] b=aacc:

a b b

Critical pair: aaacc=1.

Defines rule #1.