 Theorem 11 (Büchi 1962; Elgot 1961; Rabin 1968) The monadic second-order theory of \((\oN,s)\), i.e., the successor function on \(\oN\) and of the full infinite binary tree, i.e., two successor functions on \(\oN\), are both decidable.