Certificate for #5629 ⟨a, b, c | aa=a, abc=bb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abc=bb

Axiom: abc=bb.

Defines rule #3.

Referenced by [3].

[3] abb=bb

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

a a abc

Critical pair: abb=abc.

Reduce RHS:

[2](abc)
⇒ bb

Defines rule #2.