Certificate for #3495 ⟨a, b, c | bb=aa, cac=b⟩

Back:⟨a, b, c | bb=aa, cac=b⟩

Completion settings:

[1] bb=aa

Axiom: bb=aa.

Referenced by [3].

[2] b=cac

Axiom: cac=b.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3].

[3] caccac=aa

Overlap of [1] bb=aa with [2] b=cac:

bb b

Critical pair: cacb=aa.

Reduce LHS:

[2]cac(b)
⇒ caccac

Defines rule #2.

Referenced by [4], [5].

[4] cacaa=aacac

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

cac cac caccac

Critical pair: cacaa=aacac.

Defines rule #1.

[5] caccaaa=aaaccac

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

cacca c caccac

Critical pair: caccaaa=aaaccac.

Defines rule #3.