Certificate for #15073 ⟨a, b | aab=ab, aaaaaa=1⟩

Back:⟨a, b | aab=ab, aaaaaa=1⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Referenced by [3].

[2] aaaaaa=1

Axiom: aaaaaa=1.

Defines rule #2.

Referenced by [3].

[3] ab=b

Overlap of [2] aaaaaa=1 with [1] aab=ab:

aaaa aa aab

Critical pair: aaaaab=b.

Reduce LHS:

[1]aaa(aab)
[1]⇒ aa(aab)
[1]⇒ a(aab)
[1]⇒ (aab)
⇒ ab

Defines rule #1.