A famous result by Rabin states that the monadic second order theory of the binary tree is decidable. By the binary tree, understand the free monoid $\{0,1\}^*$ of words, with operations $S_0(w)=w0$ and $S_1(w)=w1$, or the set $\{1,2,\dots\}=\mathbb N$ of naturals with operations $S_i(n)=2n+i$.
I would like to know if the same is true for a kind of "backwards-growing" tree: the union of all height-$s$ binary trees with the root moving away to infinity. Formally, it can be described as the set $\mathbb N$ of naturals with partially-defined operations $S_0(n)=n-2^{s-1}$ and $S_1(n)=n+2^{s-1}$ if $n=2^s(2m+1)$ (so they're defined only if $s>0$). The span of $2^s(2m+1)$ is a height-$s$ binary tree, with leaves the odd numbers, reached from numbers $\equiv2\pmod4$, reached from numbers $\equiv4\pmod8$, etc.
Certainly the theory is not the same as that of the binary tree --- even the first-order logic is different, since odd numbers have no successor. However, I suspect that, just as for the usual tree, the monadic second-order theory is decidable.
Good pointers to the literature would also be most welcome!
