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.