:: deftheorem defines is_valid_output NOMIN_8:def 12 :
for V, A being set
for d being object
for Z, res being FinSequence holds
( res is_valid_output V,A,Z,d iff ex d1 being NonatomicND of V,A st
( d = d1 & Z is_valid_wrt d1 & ( for n being Nat st 1 <= n & n <= len Z holds
d1 . (Z . n) = res . n ) ) );