Decidability via Mosaics for Bundled Ockhamist Logic

We adapt the 'mosaics' technique of Reynolds 1997 (in turn an adaption of Nemeti 1986) achieving decidability for the (non local) Ockhamist logic of (upward endless) bundled trees. We produce a double exponential time procedure, thus improving the complexity upper bound of the problem - so far relying on the non elementary procedure of the Rabin's Theorem (Burgess 1979).