:: Algorithm NextFit for the Bin Packing Problem
:: by Hiroshi Fujiwara , Ryota Adachi and Hiroaki Yamamoto
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users


definition
let a be non empty FinSequence of REAL ;
let i be Element of dom a;
:: original: .
redefine func a . i -> Element of REAL ;
correctness
coherence
a . i is Element of REAL ;
proof end;
end;

definition
let h be non empty FinSequence of NAT * ;
let i be Element of dom h;
:: original: .
redefine func h . i -> FinSequence of NAT ;
correctness
coherence
h . i is FinSequence of NAT ;
proof end;
end;

theorem NF992: :: BINPACK1:1
for n being Nat st n is odd holds
( 1 <= n & (n + 1) div 2 = (n + 1) / 2 )
proof end;

theorem NF315: :: BINPACK1:2
for D being set
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D
proof end;

theorem NF501: :: BINPACK1:3
for x, y being object holds {[x,y]} " {y} = {x}
proof end;

theorem NF600: :: BINPACK1:4
for a, b being Nat
for s being set holds
( not (Seg a) \/ {s} = Seg b or a = b or a + 1 = b )
proof end;

definition
let D be non empty set ;
let f be D -valued FinSequence;
let I be set ;
::: assume I c= dom f; :: not needed to prove the correctness of definition
func Seq (f,I) -> D -valued FinSequence equals :: BINPACK1:def 1
 Seq (f | I);
coherence
Seq (f | I) is D -valued FinSequence ;
end;

:: deftheorem defines Seq BINPACK1:def 1 :
for D being non empty set
for f being b1 -valued FinSequence
for I being set holds Seq (f,I) = Seq (f | I);

definition
let a be non empty FinSequence of REAL ;
let f be Function;
let s be set ;
func SumBin (a,f,s) -> Real equals :: BINPACK1:def 2
 Sum (Seq (a,(f " s)));
coherence
Sum (Seq (a,(f " s))) is Real ;
end;

:: deftheorem defines SumBin BINPACK1:def 2 :
for a being non empty FinSequence of REAL
for f being Function
for s being set holds SumBin (a,f,s) = Sum (Seq (a,(f " s)));

registration
cluster Relation-like NAT -defined REAL -valued Function-like non empty finite complex-valued ext-real-valued real-valued FinSequence-like FinSubsequence-like positive for FinSequence of REAL ;
existence
ex b1 being non empty FinSequence of REAL st b1 is positive
proof end;
end;

definition
let a be FinSequence of REAL ;
attr a is at_most_one means :: BINPACK1:def 3
 for i being Nat st 1 <= i & i <= len a holds
a . i <= 1;
end;

:: deftheorem defines at_most_one BINPACK1:def 3 :
for a being FinSequence of REAL holds
( a is at_most_one iff for i being Nat st 1 <= i & i <= len a holds
a . i <= 1 );

registration
cluster Relation-like NAT -defined REAL -valued Function-like non empty finite complex-valued ext-real-valued real-valued FinSequence-like FinSubsequence-like positive at_most_one for FinSequence of REAL ;
existence
ex b1 being non empty positive FinSequence of REAL st b1 is at_most_one
proof end;
end;

theorem NF100: :: BINPACK1:5
for f being FinSequence of NAT
for j, b being Nat st b = j holds
(f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)}
proof end;

theorem NF110: :: BINPACK1:6
for f being FinSequence of NAT
for j, b being Nat st b <> j holds
(f ^ <*b*>) " {j} = f " {j}
proof end;

theorem NF120: :: BINPACK1:7
for a being non empty FinSequence of REAL
for p being set
for i being Nat st p \/ {i} c= dom a & ( for m being Nat st m in p holds
m < i ) holds
Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>
proof end;

theorem NF200: :: BINPACK1:8
for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for j, b being Nat st (len f) + 1 <= len a & b = j holds
SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1))
proof end;

theorem :: BINPACK1:9
for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for j, b being Nat st (len f) + 1 <= len a & b <> j holds
SumBin (a,(f ^ <*b*>),{j}) = SumBin (a,f,{j}) by NF110;

theorem NF260: :: BINPACK1:10
for a being non empty FinSequence of REAL
for f being FinSequence of NAT st dom f = dom a holds
SumBin (a,f,(rng f)) = Sum a
proof end;

theorem NF270: :: BINPACK1:11
for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for s, t being set st s misses t holds
SumBin (a,f,(s \/ t)) = (SumBin (a,f,s)) + (SumBin (a,f,t))
proof end;

theorem NF280: :: BINPACK1:12
for a being non empty positive FinSequence of REAL
for f being FinSequence of NAT
for s being set holds 0 <= SumBin (a,f,s)
proof end;

theorem NF290: :: BINPACK1:13
for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for s being set st s misses rng f holds
SumBin (a,f,s) = 0
proof end;

theorem NF300: :: BINPACK1:14
for a being non empty at_most_one FinSequence of REAL ex k being Nat ex f being non empty FinSequence of NAT st
( dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) & k = card (rng f) )
proof end;

theorem NF305: :: BINPACK1:15
for a being non empty FinSequence of REAL
for f being FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
ex fr being FinSequence of NAT st
( dom fr = dom a & ( for j being Nat st j in rng fr holds
SumBin (a,fr,{j}) <= 1 ) & ex k being Nat st rng fr = Seg k & card (rng f) = card (rng fr) )
proof end;

LM003: for a being non empty at_most_one FinSequence of REAL ex opt being Element of NAT ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & opt = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
opt <= card (rng f) ) )
proof end;

LM004: for a being non empty at_most_one FinSequence of REAL
for opt1, opt2 being Element of NAT st ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & opt1 = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
opt1 <= card (rng f) ) ) & ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & opt2 = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
opt2 <= card (rng f) ) ) holds
opt1 = opt2
proof end;

definition
let a be non empty at_most_one FinSequence of REAL ;
func Opt a -> Element of NAT means :defOpt: :: BINPACK1:def 4
 ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & it = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
it <= card (rng f) ) );
existence
ex b1 being Element of NAT ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & b1 = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
b1 <= card (rng f) ) ) by LM003;
uniqueness
for b1, b2 being Element of NAT st ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & b1 = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
b1 <= card (rng f) ) ) & ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & b2 = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
b2 <= card (rng f) ) ) holds
b1 = b2 by LM004;
end;

:: deftheorem defOpt defines Opt BINPACK1:def 4 :
for a being non empty at_most_one FinSequence of REAL
for b2 being Element of NAT holds
( b2 = Opt a iff ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & b2 = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
b2 <= card (rng f) ) ) );

theorem NF310: :: BINPACK1:16
for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for k being Nat
for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ) holds
Sum R1 = SumBin (a,f,(rng f))
proof end;

theorem NF320: :: BINPACK1:17
for a being non empty FinSequence of REAL
for f being FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
[/(Sum a)\] <= card (rng f)
proof end;

theorem NF330: :: BINPACK1:18
for a being non empty at_most_one FinSequence of REAL holds [/(Sum a)\] <= Opt a
proof end;

LM001: for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT ex h being non empty FinSequence of NAT * st
( len h = len a & h . 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 = h . i & h . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) )
proof end;

LM002: for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT
for f, y being non empty FinSequence of NAT * st len f = len a & f . 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 = f . i & f . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) & len y = len a & y . 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 = y . i & y . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) holds
f = y
proof end;

definition
let a be non empty FinSequence of REAL ;
let Alg be Function of [:REAL,(NAT *):],NAT;
func OnlinePackingHistory (a,Alg) -> non empty FinSequence of NAT * means :defPackHistory: :: BINPACK1:def 5
( len it = len a & it . 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 = it . i & it . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) );
existence
ex b1 being non empty FinSequence of NAT * st
( len b1 = len a & b1 . 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 = b1 . i & b1 . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) ) by LM001;
uniqueness
for b1, b2 being non empty FinSequence of NAT * st len b1 = len a & b1 . 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 = b1 . i & b1 . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) & len b2 = len a & b2 . 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 = b2 . i & b2 . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) holds
b1 = b2 by LM002;
end;

:: deftheorem defPackHistory defines OnlinePackingHistory BINPACK1:def 5 :
for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT
for b3 being non empty FinSequence of NAT * holds
( b3 = OnlinePackingHistory (a,Alg) iff ( len b3 = len a & b3 . 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 = b3 . i & b3 . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) ) );

theorem :: BINPACK1:19
for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT holds (OnlinePackingHistory (a,Alg)) . 1 = {[1,1]} by defPackHistory;

theorem NF502: :: BINPACK1:20
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
SumBin (a,(h . 1),{((h . 1) . 1)}) = a . 1
proof end;

theorem NF505: :: BINPACK1:21
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
h . i is FinSequence of NAT
proof end;

theorem NF510: :: BINPACK1:22
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
len (h . i) = i
proof end;

theorem NF520: :: BINPACK1:23
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
( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) )
proof end;

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))}
proof end;

theorem NF530: :: BINPACK1:25
for a being non empty positive 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, l being Nat st 1 <= i & i < len a holds
SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})
proof end;

LM008: for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT holds (OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg))) is non empty FinSequence of NAT
proof end;

definition
let a be non empty FinSequence of REAL ;
let Alg be Function of [:REAL,(NAT *):],NAT;
func OnlinePacking (a,Alg) -> non empty FinSequence of NAT equals :: BINPACK1:def 6
(OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg)));
coherence
(OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg))) is non empty FinSequence of NAT by LM008;
end;

:: deftheorem defines OnlinePacking BINPACK1:def 6 :
for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT holds OnlinePacking (a,Alg) = (OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg)));

theorem NF540: :: BINPACK1:26
for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT
for h being non empty FinSequence of NAT *
for f being non empty FinSequence of NAT holds dom (OnlinePacking (a,Alg)) = dom a
proof end;

LM020: for a being non empty FinSequence of REAL ex nf being Function of [:REAL,(NAT *):],NAT st
for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf . (s,f) = (f . (len f)) + 1 ) )
proof end;

LM021: for a being non empty FinSequence of REAL
for nf1, nf2 being Function of [:REAL,(NAT *):],NAT st ( for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf1 . (s,f) = (f . (len f)) + 1 ) ) ) & ( for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf2 . (s,f) = (f . (len f)) + 1 ) ) ) holds
nf1 = nf2
proof end;

definition
let a be non empty FinSequence of REAL ;
func NextFit a -> Function of [:REAL,(NAT *):],NAT means :defNextFit: :: BINPACK1:def 7
 for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies it . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies it . (s,f) = (f . (len f)) + 1 ) );
existence
ex b1 being Function of [:REAL,(NAT *):],NAT st
for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b1 . (s,f) = (f . (len f)) + 1 ) ) by LM020;
uniqueness
for b1, b2 being Function of [:REAL,(NAT *):],NAT st ( for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b1 . (s,f) = (f . (len f)) + 1 ) ) ) & ( for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b2 . (s,f) = (f . (len f)) + 1 ) ) ) holds
b1 = b2 by LM021;
end;

:: deftheorem defNextFit defines NextFit BINPACK1:def 7 :
for a being non empty FinSequence of REAL
for b2 being Function of [:REAL,(NAT *):],NAT holds
( b2 = NextFit a iff for s being Real
for f being FinSequence of NAT holds
( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b2 . (s,f) = (f . (len f)) + 1 ) ) );

theorem NF805: :: BINPACK1:27
for a being non empty FinSequence of REAL
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,(NextFit a)) holds
for i being Nat st 1 <= i & i <= len a holds
ex k being Nat st
( rng (h . i) = Seg k & (h . i) . i = k )
proof end;

theorem NF880: :: BINPACK1:28
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 being Nat st 1 <= i & i <= len a holds
SumBin (a,(h . i),{((h . i) . i)}) <= 1
proof end;

theorem NF890: :: BINPACK1:29
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 being Nat st 1 <= i & i <= len a & j in rng (h . i) holds
SumBin (a,(h . i),{j}) <= 1
proof end;

theorem :: BINPACK1:30
for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds
for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1
proof end;

theorem NF807: :: BINPACK1:31
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, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds
(h . i) . i = k
proof end;

theorem NF815: :: BINPACK1:32
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, k being Nat st 1 <= i & i < len a & rng (h . i) = Seg k & rng (h . (i + 1)) = Seg (k + 1) holds
(SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1
proof end;

theorem NF820: :: BINPACK1:33
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, l, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k & 2 <= k & 1 <= l & l < k holds
(SumBin (a,(h . i),{l})) + (SumBin (a,(h . i),{(l + 1)})) > 1
proof end;

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
proof end;

theorem NF910: :: BINPACK1:35
for a being non empty positive at_most_one FinSequence of REAL
for h being non empty FinSequence of NAT *
for f being FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds
ex k being Nat st rng f = Seg k
proof end;

theorem NF950: :: BINPACK1:36
for a being non empty positive at_most_one FinSequence of REAL
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
proof end;

theorem NF960: :: BINPACK1:37
for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT
for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds
k div 2 < Sum a
proof end;

theorem NF980: :: BINPACK1:38
for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT
for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds
k <= (2 * [/(Sum a)\]) - 1
proof end;

theorem :: BINPACK1:39
for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT
for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds
k <= (2 * (Opt a)) - 1
proof end;

theorem NF993: :: BINPACK1:40
for n being Nat
for epsilon being Real
for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds
( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) & f = OnlinePacking (a,(NextFit a)) holds
n = card (rng f)
proof end;

theorem NF994: :: BINPACK1:41
for n being Nat
for epsilon being Real
for a being non empty positive at_most_one FinSequence of REAL st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds
( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) holds
Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)
proof end;

theorem NF996: :: BINPACK1:42
for n being Nat
for epsilon being Real
for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds
( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) & dom f = dom a & ( for i being Nat st i in Seg n holds
( ( i is odd implies f . i = 1 ) & ( i is even implies f . i = (i div 2) + 1 ) ) ) holds
for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1
proof end;

theorem NF997: :: BINPACK1:43
for n being Nat
for epsilon being Real
for a being non empty positive at_most_one FinSequence of REAL st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds
( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) holds
n = (2 * (Opt a)) - 1
proof end;

theorem :: BINPACK1:44
for n being Nat st n is odd holds
ex a being non empty positive at_most_one FinSequence of REAL st
( len a = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds
( n = card (rng f) & n = (2 * (Opt a)) - 1 ) ) )
proof end;