theorem NF525: :: BINPACK1:24

for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds
for i being Nat st 1 <= i & i < len a holds
rng (h . (i + 1)) = (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))}