:: deftheorem defines OnlinePacking BINPACK1:def 6 :
for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT holds OnlinePacking (a,Alg) = (OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg)));