On algorithmic properties of finite subset algebra for some unoids

We consider unoids consisting of identical non-branching trees which are connected into an infinite line. We establish that the finite subset algebra admits effective quantifier elimination and it does not depend on the original algebra. So, we have an instance where the finite subset algebra theory is algorithmically simpler than the theory of the original one. Also it demonstrates that the union operation for finite subset algebras does matter for algorithmical properties.