:: deftheorem defNextFit defines NextFit BINPACK1:def 7 :
for a being non empty FinSequence of REAL
for b₂ being Function of [:REAL,(NAT *):],NAT holds
( b₂ = NextFit a iff for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b₂ . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b₂ . (s,f) = (f . (len f)) + 1 ) ) );