I've been reading Rabin's article on decidability in Barwise's text, and I came across Rabin's discussion of the decidability proof of his tree theory: the second-order theory with two successor functions. The text mentions that the proof is hard and very technical owing to many extensions of automata theory, and I was wondering if someone might be able to sketch it out.

Thanks!