Phil Wadler suggests some proofs to show the correspondence of the decidable definition of FD to the more clearly semantically valid pureFD.