Certificate for #11133 ⟨a, b | aaaaa=b, bbbbb=1⟩

Completion settings:

[1] b=aaaaa

Axiom: aaaaa=b.

Flip LHS and RHS.

Defines rule #2.

Referenced by [2].

[2] aaaaaaaaaaaaaaaaaaaaaaaaa=1

Axiom: bbbbb=1.

Reduce LHS:

[1](b)bbbb
[1]⇒ aaaaa(b)bbb
[1]⇒ aaaaaaaaaa(b)bb
[1]⇒ aaaaaaaaaaaaaaa(b)b
[1]⇒ aaaaaaaaaaaaaaaaaaaa(b)
⇒ aaaaaaaaaaaaaaaaaaaaaaaaa

Defines rule #1.