Certificate for #2804 ⟨a, b, c | aaa=a, abc=b⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #2.

Referenced by [3].

[2] abc=b

Axiom: abc=b.

Referenced by [3], [4].

[3] aab=b

Overlap of [1] aaa=a with [2] abc=b:

aa a abc

Critical pair: aab=abc.

Reduce RHS:

[2](abc)
⇒ b

Defines rule #3.

Referenced by [4].

[4] bc=ab

Overlap of [3] aab=b with [2] abc=b:

a ab abc

Critical pair: ab=bc.

Flip LHS and RHS.

Defines rule #1.