let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: for f being non empty FinSequence of NAT

for k being Nat st f = OnlinePacking (a,(NextFit a)) & rng f = Seg k holds

for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & rng f = Seg k holds

for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & rng f = Seg k implies for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 )

assume that

HL00: f = OnlinePacking (a,(NextFit a)) and

BN00: rng f = Seg k ; :: thesis: for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

set h = OnlinePackingHistory (a,(NextFit a));

let j be Nat; :: thesis: ( 1 <= j & j <= k div 2 implies (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 )

assume that

L202: 1 <= j and

L203: j <= k div 2 ; :: thesis: (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

k <> 0 by BN00;

for k being Nat st f = OnlinePacking (a,(NextFit a)) & rng f = Seg k holds

for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & rng f = Seg k holds

for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & rng f = Seg k implies for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 )

assume that

HL00: f = OnlinePacking (a,(NextFit a)) and

BN00: rng f = Seg k ; :: thesis: for j being Nat st 1 <= j & j <= k div 2 holds

(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

set h = OnlinePackingHistory (a,(NextFit a));

let j be Nat; :: thesis: ( 1 <= j & j <= k div 2 implies (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 )

assume that

L202: 1 <= j and

L203: j <= k div 2 ; :: thesis: (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

k <> 0 by BN00;

per cases then
( k = 1 or 2 <= k )
by NAT_1:23;

end;

suppose
k = 1
; :: thesis: (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

hence
(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1
by NAT_D:27, L202, L203; :: thesis: verum

end;suppose L60:
2 <= k
; :: thesis: (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

set i = len (OnlinePackingHistory (a,(NextFit a)));

L220: len (OnlinePackingHistory (a,(NextFit a))) = len a by defPackHistory;

1 <= len (OnlinePackingHistory (a,(NextFit a))) by NAT_1:14;

hence (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 by L220, NF830, L60, L202, L203, HL00, BN00; :: thesis: verum

end;L220: len (OnlinePackingHistory (a,(NextFit a))) = len a by defPackHistory;

1 <= len (OnlinePackingHistory (a,(NextFit a))) by NAT_1:14;

hence (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 by L220, NF830, L60, L202, L203, HL00, BN00; :: thesis: verum