:: deftheorem defines valid_output NOMIN_8:def 13 :
for V, A being set
for Z, res being object
for b₅ being SCPartialNominativePredicate of V,A holds
( b₅ = valid_output (V,A,Z,res) iff ( dom b₅ = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,Z)) } & ( for d being object st d in dom b₅ holds
( ( <*res*> is_valid_output V,A,<*Z*>,d implies b₅ . d = TRUE ) & ( not <*res*> is_valid_output V,A,<*Z*>,d implies b₅ . d = FALSE ) ) ) ) );