Certificate for #4827 ⟨a, b | abababba=baa⟩

Back:⟨a, b | abababba=baa⟩

Completion settings:

[1] abababba=baa

Axiom: abababba=baa.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

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

[3] baa=cccba

Overlap of [1] abababba=baa with [2] ab=c:

abababba ab

Critical pair: cababba=baa.

Reduce LHS:

[2]c(ab)abba
[2]⇒ cc(ab)ba
⇒ cccba

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] caa=acccba

Overlap of [2] ab=c with [3] baa=cccba:

a b baa

Critical pair: acccba=caa.

Flip LHS and RHS.

Defines rule #5.

[5] bac=cccbc

Overlap of [3] baa=cccba with [2] ab=c:

ba a ab

Critical pair: bac=cccbab.

Reduce RHS:

[2]cccb(ab)
⇒ cccbc

Defines rule #2.

Referenced by [6].

[6] cac=acccbc

Overlap of [2] ab=c with [5] bac=cccbc:

a b bac

Critical pair: acccbc=cac.

Flip LHS and RHS.

Defines rule #3.