Certificate for #12454 ⟨a, b | aabb=ab, abaa=a⟩

Back:⟨a, b | aabb=ab, abaa=a⟩

Completion settings:

[1] aabb=ab

Axiom: aabb=ab.

Referenced by [4].

[2] abaa=a

Axiom: abaa=a.

Referenced by [6].

[3] ab=c

Axiom: ab=c.

Defines rule #1.

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

[4] aabb=c

Simplify [1] aabb=ab.

Reduce RHS:

[3](ab)
⇒ c

Referenced by [5].

[5] acb=c

Overlap of [4] aabb=c with [3] ab=c:

a abb ab

Critical pair: acb=c.

Referenced by [8], [9].

[6] caa=a

Overlap of [2] abaa=a with [3] ab=c:

abaa ab

Critical pair: caa=a.

Defines rule #5.

Referenced by [7], [10].

[7] cac=c

Overlap of [6] caa=a with [3] ab=c:

ca a ab

Critical pair: cac=ab.

Reduce RHS:

[3](ab)
⇒ c

Defines rule #6.

Referenced by [8].

[8] cb=cc

Overlap of [7] cac=c with [5] acb=c:

c ac acb

Critical pair: cc=cb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[9] acc=c

Overlap of [5] acb=c with [8] cb=cc:

a cb cb

Critical pair: acc=c.

Defines rule #4.

Referenced by [10].

[10] aca=a

Overlap of [9] acc=c with [6] caa=a:

ac c caa

Critical pair: aca=caa.

Reduce RHS:

[6](caa)
⇒ a

Defines rule #3.