Certificate for #5633 ⟨a, b, c | aa=a, abc=cc⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abc=cc

Axiom: abc=cc.

Defines rule #2.

Referenced by [3].

[3] acc=cc

Overlap of [1] aa=a with [2] abc=cc:

a a abc

Critical pair: acc=abc.

Reduce RHS:

[2](abc)
⇒ cc

Defines rule #3.