:: deftheorem defPackHistory defines OnlinePackingHistory BINPACK1:def 5 :
for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT
for b₃ being non empty FinSequence of NAT * holds
( b₃ = OnlinePackingHistory (a,Alg) iff ( len b₃ = len a & b₃ . 1 = <*1*> & ( for i being Nat st 1 <= i & i < len a holds
ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = b₃ . i & b₃ . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) ) );