:: 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 b₁ -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 b₁ being non empty FinSequence of REAL st b₁ 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 b₁ being non empty positive FinSequence of REAL st b₁ 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 b₁ 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 ) & b₁ = 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
b₁ <= card (rng f) ) ) by LM003;
uniqueness
for b₁, b₂ 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 ) & b₁ = 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
b₁ <= 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 ) & b₂ = 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
b₂ <= card (rng f) ) ) holds
b₁ = b₂ by LM004;

end;

:: deftheorem defOpt defines Opt BINPACK1:def 4 :
for a being non empty at_most_one FinSequence of REAL
for b₂ being Element of NAT holds
( b₂ = 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 ) & b₂ = 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
b₂ <= 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 b₁ being non empty FinSequence of NAT * st
( len b₁ = len a & b₁ . 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 = b₁ . i & b₁ . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) ) by LM001;
uniqueness
for b₁, b₂ being non empty FinSequence of NAT * st len b₁ = len a & b₁ . 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 = b₁ . i & b₁ . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) & len b₂ = len a & b₂ . 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 = b₂ . i & b₂ . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) holds
b₁ = b₂ 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 b₃ being non empty FinSequence of NAT * holds
( b₃ = OnlinePackingHistory (a,Alg) iff ( len b₃ = len a & b₃ . 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 = b₃ . i & b₃ . (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 b₁ 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 b₁ . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b₁ . (s,f) = (f . (len f)) + 1 ) ) by LM020;
uniqueness
for b₁, b₂ 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 b₁ . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b₁ . (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 b₂ . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b₂ . (s,f) = (f . (len f)) + 1 ) ) ) holds
b₁ = b₂ by LM021;

end;

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