Certificate for #7335 ⟨a, b, c | ab=1, aacc=bb⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Referenced by [3], [5].

[2] bb=aacc

Axiom: aacc=bb.

Flip LHS and RHS.

Referenced by [3], [4].

[3] b=aaacc

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

a b bb

Critical pair: aaacc=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] aaccaaacc=aaaccaacc

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

b b bb

Critical pair: baacc=aaccb.

Reduce LHS:

[3](b)aacc
⇒ aaaccaacc

Reduce RHS:

[3]aacc(b)
⇒ aaccaaacc

Flip LHS and RHS.

Defines rule #2.

[5] aaaacc=1

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

a b b

Critical pair: aaaacc=1.

Defines rule #1.