Certificate for #919 ⟨a, b | aa=b, bbbb=b⟩

Back:⟨a, b | aa=b, bbbb=b⟩

Completion settings:

[1] b=aa

Axiom: aa=b.

Flip LHS and RHS.

Defines rule #2.

Referenced by [2].

[2] aaaaaaaa=aa

Axiom: bbbb=b.

Reduce LHS:

[1](b)bbb
[1]⇒ aa(b)bb
[1]⇒ aaaa(b)b
[1]⇒ aaaaaa(b)
⇒ aaaaaaaa

Reduce RHS:

[1](b)
⇒ aa

Defines rule #1.