theorem NF830: :: BINPACK1:34

for a being non empty positive at_most_one FinSequence of REAL
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,(NextFit a)) holds
for i, j, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k & 2 <= k & 1 <= j & j <= k div 2 holds
(SumBin (a,(h . i),{((2 * j) - 1)})) + (SumBin (a,(h . i),{(2 * j)})) > 1