[Haskell] looking for interesting examples with recursion + state in which you'd want to prove termination

Hi Haskell folks, I'm looking for interesting recursive functions (i.e. not tail-recursive) that make use of state in the state monad. I'd like to prove them terminating with a new method I'm developing (or, of course, perhaps disprove termination....). If you have examples in this class that you wouldn't mind sharing, please send them to me. - Byron http://research.microsoft.com/~bycook