Certificate for #5207 ⟨a, b, c | aa=b, acbc=c⟩

Back:⟨a, b, c | aa=b, acbc=c⟩

Completion settings:

[1] b=aa

Axiom: aa=b.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2].

[2] acaac=c

Axiom: acbc=c.

Reduce LHS:

[1]ac(b)c
⇒ acaac

Referenced by [3], [4], [5].

[3] caac=acac

Overlap of [2] acaac=c with [2] acaac=c:

aca ac acaac

Critical pair: acac=caac.

Flip LHS and RHS.

Referenced by [4], [5], [6].

[4] cac=acc

Overlap of [3] caac=acac with [2] acaac=c:

ca ac acaac

Critical pair: cac=acacaac.

Reduce RHS:

[2]ac(acaac)
⇒ acc

Defines rule #1.

Referenced by [5], [6].

[5] aaacc=c

Overlap of [2] acaac=c with [3] caac=acac:

a caac caac

Critical pair: aacac=c.

Reduce LHS:

[4]aa(cac)
⇒ aaacc

Defines rule #3.

[6] caac=aacc

Simplify [3] caac=acac.

Reduce RHS:

[4]a(cac)
⇒ aacc

Defines rule #2.