Certificate for #1846 ⟨a, b, c | aba=ac, ccb=1⟩

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

Completion settings:

[1] ac=aba

Axiom: aba=ac.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[2] ccb=1

Axiom: ccb=1.

Defines rule #4.

Referenced by [3].

[3] ababab=a

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

a c ccb

Critical pair: a=abacb.

Reduce RHS:

[1]ab(ac)b
⇒ ababab

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] aab=aba

Overlap of [3] ababab=a with [3] ababab=a:

ab abab ababab

Critical pair: aba=aab.

Flip LHS and RHS.

Defines rule #1.