Decidability of second-order theories and automata on infinite trees

In this note we announce the solvability of the decision problem of the (monadic) second-order theory of two suc- cessor functions (S2S). This answers a question raised by Büchi.