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