See also the XMonad module X.A.Navigation2D which includes formal proofs of the navigational strategies:

PDF: https://web.cs.dal.ca/~nzeh/xmonad/Navigation2D.pdf

Module: https://hackage.haskell.org/package/xmonad-contrib-0.13/docs...