Certificate for #3397 ⟨a, b, c | ac=ab, bba=c⟩

Back:⟨a, b, c | ac=ab, bba=c⟩

Completion settings:

[1] ab=ac

Axiom: ac=ab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3], [4].

[2] bba=c

Axiom: bba=c.

Defines rule #3.

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

[3] acba=ac

Overlap of [1] ab=ac with [2] bba=c:

a b bba

Critical pair: ac=acba.

Flip LHS and RHS.

Referenced by [6].

[4] cb=cc

Overlap of [2] bba=c with [1] ab=ac:

bb a ab

Critical pair: bbac=cb.

Reduce LHS:

[2](bba)c
⇒ cc

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6].

[5] ccca=cc

Overlap of [4] cb=cc with [2] bba=c:

c b bba

Critical pair: cc=ccba.

Reduce RHS:

[4]c(cb)a
⇒ ccca

Flip LHS and RHS.

Defines rule #5.

[6] acca=ac

Simplify [3] acba=ac.

Reduce LHS:

[4]a(cb)a
⇒ acca

Defines rule #4.