:: deftheorem defines SemanticFloydHoareTriples NOMIN_3:def 4 :
for D being non empty set holds SemanticFloydHoareTriples D = { <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE } ;