Certificate for #5521 ⟨a, b, c | ab=c, abba=c⟩

Back:⟨a, b, c | ab=c, abba=c⟩

Completion settings:

[1] ab=c

Axiom: ab=c.

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

[2] cba=c

Axiom: abba=c.

Reduce LHS:

[1](ab)ba
⇒ cba

Referenced by [4].

[3] cb=d

Axiom: cb=d.

Referenced by [4], [5].

[4] c=da

Overlap of [2] cba=c with [3] cb=d:

cba cb

Critical pair: da=c.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6].

[5] dda=d

Overlap of [3] cb=d with [4] c=da:

cb c

Critical pair: dab=d.

Reduce LHS:

[1]d(ab)
[4]⇒ d(c)
⇒ dda

Defines rule #1.

Referenced by [7].

[6] ab=da

Simplify [1] ab=c.

Reduce RHS:

[4](c)
⇒ da

Defines rule #3.

Referenced by [7].

[7] db=dd

Overlap of [5] dda=d with [6] ab=da:

dd a ab

Critical pair: ddda=db.

Reduce LHS:

[5]d(dda)
⇒ dd

Flip LHS and RHS.

Defines rule #4.