Inference of the Definition of the Predicate Transformer wp with Occurrences of the Predicate Domain Based on Denotational Semantics of GCL on ZF Set Theory.