:: 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 ;

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

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 ;

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

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

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;

definition

let D be non empty set ;

let f be D -valued FinSequence;

let I be set ;

Seq (f | I) is D -valued FinSequence ;

end;
let f be D -valued FinSequence;

let I be set ;

::: assume I c= dom f; :: not needed to prove the correctness of definition

coherence Seq (f | I) is D -valued FinSequence ;

:: deftheorem defines Seq BINPACK1:def 1 :

for D being non empty set

for f being b_{1} -valued FinSequence

for I being set holds Seq (f,I) = Seq (f | I);

for D being non empty set

for f being b

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 ;

coherence

Sum (Seq (a,(f " s))) is Real ;

end;
let f be Function;

let s be set ;

coherence

Sum (Seq (a,(f " s))) is Real ;

:: 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)));

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

ex b_{1} being non empty FinSequence of REAL st b_{1} is positive
end;

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

proof end;

definition

let a be FinSequence of REAL ;

end;
attr a is at_most_one means :: BINPACK1:def 3

for i being Nat st 1 <= i & i <= len a holds

a . i <= 1;

for i being Nat st 1 <= i & i <= len a holds

a . i <= 1;

:: 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 );

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

ex b_{1} being non empty positive FinSequence of REAL st b_{1} is at_most_one
end;

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

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

for j, b being Nat st b = j holds

(f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)}

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)*>

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))

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

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

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))

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)

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

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) )

( 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) )

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 ;

ex b_{1} 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_{1} = 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_{1} <= card (rng f) ) )
by LM003;

uniqueness

for b_{1}, b_{2} 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_{1} = 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_{1} <= 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_{2} = 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_{2} <= card (rng f) ) ) holds

b_{1} = b_{2}
by LM004;

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

ex b

( dom g = dom a & ( for j being Nat st j in rng g holds

SumBin (a,g,{j}) <= 1 ) & b

SumBin (a,f,{j}) <= 1 ) holds

b

uniqueness

for b

( dom g = dom a & ( for j being Nat st j in rng g holds

SumBin (a,g,{j}) <= 1 ) & b

SumBin (a,f,{j}) <= 1 ) holds

b

( dom g = dom a & ( for j being Nat st j in rng g holds

SumBin (a,g,{j}) <= 1 ) & b

SumBin (a,f,{j}) <= 1 ) holds

b

b

:: deftheorem defOpt defines Opt BINPACK1:def 4 :

for a being non empty at_most_one FinSequence of REAL

for b_{2} being Element of NAT holds

( b_{2} = 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_{2} = 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_{2} <= card (rng f) ) ) );

for a being non empty at_most_one FinSequence of REAL

for b

( b

( dom g = dom a & ( for j being Nat st j in rng g holds

SumBin (a,g,{j}) <= 1 ) & b

SumBin (a,f,{j}) <= 1 ) holds

b

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))

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)

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;

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;

ex b_{1} being non empty FinSequence of NAT * st

( len b_{1} = len a & b_{1} . 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_{1} . i & b_{1} . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) )
by LM001;

uniqueness

for b_{1}, b_{2} being non empty FinSequence of NAT * st len b_{1} = len a & b_{1} . 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_{1} . i & b_{1} . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) & len b_{2} = len a & b_{2} . 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_{2} . i & b_{2} . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) holds

b_{1} = b_{2}
by LM002;

end;
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 ( 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))*> ) ) );

ex b

( len b

ex d1 being Element of REAL ex d2 being FinSequence of NAT st

( d1 = a . (i + 1) & d2 = b

uniqueness

for b

ex d1 being Element of REAL ex d2 being FinSequence of NAT st

( d1 = a . (i + 1) & d2 = b

ex d1 being Element of REAL ex d2 being FinSequence of NAT st

( d1 = a . (i + 1) & d2 = b

b

:: 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_{3} being non empty FinSequence of NAT * holds

( b_{3} = OnlinePackingHistory (a,Alg) iff ( len b_{3} = len a & b_{3} . 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_{3} . i & b_{3} . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) ) );

for a being non empty FinSequence of REAL

for Alg being Function of [:REAL,(NAT *):],NAT

for b

( b

ex d1 being Element of REAL ex d2 being FinSequence of NAT st

( d1 = a . (i + 1) & d2 = b

theorem :: BINPACK1:19

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

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

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

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)) )

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))}

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})

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;

(OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg))) is non empty FinSequence of NAT by LM008;

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

(OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg))) is non empty FinSequence of NAT by LM008;

:: 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)));

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

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 ;

ex b_{1} 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_{1} . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b_{1} . (s,f) = (f . (len f)) + 1 ) )
by LM020;

uniqueness

for b_{1}, b_{2} 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_{1} . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b_{1} . (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_{2} . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b_{2} . (s,f) = (f . (len f)) + 1 ) ) ) holds

b_{1} = b_{2}
by LM021;

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

ex b

for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b

uniqueness

for b

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b

b

:: deftheorem defNextFit defines NextFit BINPACK1:def 7 :

for a being non empty FinSequence of REAL

for b_{2} being Function of [:REAL,(NAT *):],NAT holds

( b_{2} = NextFit a iff for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b_{2} . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies b_{2} . (s,f) = (f . (len f)) + 1 ) ) );

for a being non empty FinSequence of REAL

for b

( b

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies b

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 )

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

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

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

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

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

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

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

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

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

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

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

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

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)

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)

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

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

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 ) ) )

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;