Certificate for #1449 ⟨a, b, c | ab=1, aac=bb⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Referenced by [3], [5].

[2] bb=aac

Axiom: aac=bb.

Flip LHS and RHS.

Referenced by [3], [4].

[3] b=aaac

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

a b bb

Critical pair: aaac=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] aacaaac=aaacaac

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

b b bb

Critical pair: baac=aacb.

Reduce LHS:

[3](b)aac
⇒ aaacaac

Reduce RHS:

[3]aac(b)
⇒ aacaaac

Flip LHS and RHS.

Defines rule #2.

[5] aaaac=1

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

a b b

Critical pair: aaaac=1.

Defines rule #1.