Certificate for #3186 ⟨a, b, c | ba=ab, abca=1⟩

Back:⟨a, b, c | ba=ab, abca=1⟩

Completion settings:

[1] ba=ab

Axiom: ba=ab.

Defines rule #1.

Referenced by [3], [5].

[2] abca=1

Axiom: abca=1.

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

[3] abbca=b

Overlap of [1] ba=ab with [2] abca=1:

b a abca

Critical pair: b=abbca.

Flip LHS and RHS.

Referenced by [5].

[4] bca=abc

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

abc a abca

Critical pair: abc=bca.

Flip LHS and RHS.

Defines rule #2.

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

[5] aabbc=b

Simplify [3] abbca=b.

Reduce LHS:

[4]ab(bca)
[1]⇒ a(ba)bc
⇒ aabbc

Referenced by [6].

[6] bbc=bcb

Overlap of [4] bca=abc with [5] aabbc=b:

bc a aabbc

Critical pair: bcb=abcabbc.

Reduce RHS:

[2](abca)bbc
⇒ bbc

Flip LHS and RHS.

Defines rule #3.

[7] aabc=1

Overlap of [2] abca=1 with [4] bca=abc:

a bca bca

Critical pair: aabc=1.

Defines rule #4.