Certificate for #1844 ⟨a, b, c | aba=ac, cbc=1⟩

Back:⟨a, b, c | aba=ac, cbc=1⟩

Completion settings:

[1] ac=aba

Axiom: aba=ac.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[2] cbc=1

Axiom: cbc=1.

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

[3] bc=cb

Overlap of [2] cbc=1 with [2] cbc=1:

cb c cbc

Critical pair: cb=bc.

Flip LHS and RHS.

Defines rule #3.

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

[4] ababab=a

Overlap of [1] ac=aba with [2] cbc=1:

a c cbc

Critical pair: a=ababc.

Reduce RHS:

[3]aba(bc)
[1]⇒ ab(ac)b
⇒ ababab

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] aab=aba

Overlap of [4] ababab=a with [3] bc=cb:

ababa b bc

Critical pair: ababacb=ac.

Reduce LHS:

[1]abab(ac)b
[4]⇒ (ababab)ab
⇒ aab

Reduce RHS:

[1](ac)
⇒ aba

Defines rule #1.

[6] ccb=1

Overlap of [2] cbc=1 with [3] bc=cb:

c bc bc

Critical pair: ccb=1.

Defines rule #5.