Certificate for #5192 ⟨a, b, c | aa=b, abcb=c⟩

Back:⟨a, b, c | aa=b, abcb=c⟩

Completion settings:

[1] b=aa

Axiom: aa=b.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2].

[2] aaacaa=c

Axiom: abcb=c.

Reduce LHS:

[1]a(b)cb
[1]⇒ aaac(b)
⇒ aaacaa

Defines rule #3.

Referenced by [3], [4].

[3] aaacc=cacaa

Overlap of [2] aaacaa=c with [2] aaacaa=c:

aaac aa aaacaa

Critical pair: aaacc=cacaa.

Defines rule #1.

[4] aaacac=caacaa

Overlap of [2] aaacaa=c with [2] aaacaa=c:

aaaca a aaacaa

Critical pair: aaacac=caacaa.

Defines rule #2.