Certificate for #5767 ⟨a, b, c | aa=b, cbc=bb⟩

Completion settings:

[1] b=aa

Axiom: aa=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [2].

[2] caac=aaaa

Axiom: cbc=bb.

Reduce LHS:

[1]c(b)c
⇒ caac

Reduce RHS:

[1](b)b
[1]⇒ aa(b)
⇒ aaaa

Defines rule #1.

Referenced by [3].

[3] caaaaaa=aaaaaac

Overlap of [2] caac=aaaa with [2] caac=aaaa:

caa c caac

Critical pair: caaaaaa=aaaaaac.

Defines rule #2.