let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: 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
let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies 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 )
assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: 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
let i, j, k be Nat; :: thesis: ( 1 <= i & i <= len a & rng (h . i) = Seg k & 2 <= k & 1 <= j & j <= k div 2 implies (SumBin (a,(h . i),{((2 * j) - 1)})) + (SumBin (a,(h . i),{(2 * j)})) > 1 )
assume that
L100: 1 <= i and
L101: i <= len a and
L200: rng (h . i) = Seg k and
L201: 2 <= k and
L202: 1 <= j and
L203: j <= k div 2 ; :: thesis: (SumBin (a,(h . i),{((2 * j) - 1)})) + (SumBin (a,(h . i),{(2 * j)})) > 1
set l = (2 * j) - 1;
L298: 2 * 1 <= 2 * j by L202, XREAL_1:64;
then L299: (2 * 1) - 1 <= (2 * j) - 1 by XREAL_1:9;
L320: k mod 2 >= 0 by INT_1:57;
((k div 2) * 2) + (k mod 2) = k by INT_1:59;
then L339: (((k div 2) * 2) + (k mod 2)) - (k mod 2) <= k - 0 by L320, XREAL_1:13;
2 * j <= 2 * (k div 2) by L203, XREAL_1:64;
then 2 * j <= k by L339, XXREAL_0:2;
then 2 * j < k + 1 by NAT_1:13;
then L399: (2 * j) - 1 < (k + 1) - 1 by XREAL_1:14;
reconsider l = (2 * j) - 1 as Nat by L298;
(SumBin (a,(h . i),{l})) + (SumBin (a,(h . i),{(l + 1)})) > 1 by HN00, L100, L101, L200, L201, L299, L399, NF820;
hence (SumBin (a,(h . i),{((2 * j) - 1)})) + (SumBin (a,(h . i),{(2 * j)})) > 1 ; :: thesis: verum