  The tree share structure proposed by Dockins et al. is an elegant model for
tracking disjoint ownership in concurrent separation logic, but decision
procedures for tree shares are hard to implement due to a lack of a systematic
theoretical study. We show that the first-order theory of the full Boolean
algebra of tree shares (that is, with all tree-share constants) is decidable
and has the same complexity as of the first-order theory of Countable Atomless
Boolean Algebras. We prove that combining this additive structure with a
constant-restricted unary multiplicative "relativization" operator has a
non-elementary lower bound. We examine the consequences of this lower bound and
prove that it comes from the combination of both theories by proving an upper
bound on a generalization of the restricted multiplicative theory in isolation.
