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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abcb=b

Axiom: abcb=b.

Referenced by [3], [4].

[3] ab=b

Overlap of [1] aa=a with [2] abcb=b:

a a abcb

Critical pair: ab=abcb.

Reduce RHS:

[2](abcb)
⇒ b

Defines rule #2.

Referenced by [4].

[4] bcb=b

Overlap of [2] abcb=b with [3] ab=b:

abcb ab

Critical pair: bcb=b.

Defines rule #3.