Finally completed a long-winded proof of the Gibbard-Satterthwaite theorem in Isabelle. This is a bit more complex than the proof of Arrow's Theorem because of the requisite ballot manipulations, though most of the ideas are the same. I followed Taylor quite closely. Of perhaps more general interest, in Section 3.3: The Equivalence of Arrow's Theorem and the Gibbard-Satterthwaite Theorem he says:
In geometry, we can say that two versions of the parallel postulate are equivalent if each becomes a theorem when the other is added as an axiom to Euclid's original four. Similarly, we say that two versions of the axiom of choice are equivalent if each becomes a theorem when the other is added as an axiom to the Zermelo-Fraenkel axioms for set theory.
The reasons these assertions have formal content is that the results whose equivalence is being claimed are independent of the remaining axioms (assuming the consistency of the remaining axioms). Absent this condition of independence, the theorem asserting that 2 + 2 = 4 would qualify as being equivalent to Andrew Wiles' elliptic curve result that settled Fermat's last theorem (each being provable from the standard axioms of set theory with the other added — or not added, as it turns out).
Equivalence, however, is also used in an informal sense inspired by the formal notion above. We say that two theorems are equivalent if each is "easily derivable" from the other, where the ease of the derivation is measured (intuitively) relative to the difficulty of the stand-alone proofs of the theorems whose equivalence is being asserted. It is in this informal sense that we want to ask about the equivalence of Arrow's theorem and the Gibbard-Satterthwaite theorem.
You'll have to read his book for his conclusions on this very important topic.
As it stands I have a grotty proof for the linear-ballots case and hope to extend it to the non-linear case in the near future.