more documentation of wd_outcome proof; simplified some proofs