Certificate for #3506 ⟨a, b, c | bb=ac, aac=b⟩

Back:⟨a, b, c | bb=ac, aac=b⟩

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Referenced by [3].

[2] b=aac

Axiom: aac=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[3] aacaac=ac

Overlap of [1] bb=ac with [2] b=aac:

bb b

Critical pair: aacb=ac.

Reduce LHS:

[2]aac(b)
⇒ aacaac

Referenced by [4], [5].

[4] acaac=aacac

Overlap of [3] aacaac=ac with [3] aacaac=ac:

aac aac aacaac

Critical pair: aacac=acaac.

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] aaacac=ac

Overlap of [3] aacaac=ac with [4] acaac=aacac:

a acaac acaac

Critical pair: aaacac=ac.

Defines rule #2.