let n be Nat; :: thesis: 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)

let epsilon be Real; :: thesis: 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)

let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: 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)

let f be non empty FinSequence of NAT ; :: thesis: ( 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)) implies n = card (rng f) )

assume that

L010: n is odd and

L030: len a = n and

L040: epsilon = 1 / (n + 1) and

L050: 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 ) ) and

HL00: f = OnlinePacking (a,(NextFit a)) ; :: thesis: n = card (rng f)

L020: 1 <= n by L010, NF992;

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

defpred S_{1}[ Nat] means ( ( $1 is odd implies SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . $1),{(((OnlinePackingHistory (a,(NextFit a))) . $1) . $1)}) = 2 * epsilon ) & ( $1 is even implies SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . $1),{(((OnlinePackingHistory (a,(NextFit a))) . $1) . $1)}) = 1 - epsilon ) & ((OnlinePackingHistory (a,(NextFit a))) . $1) . $1 = $1 & rng ((OnlinePackingHistory (a,(NextFit a))) . $1) = Seg $1 );

L300: S_{1}[1]
_{1}[i] holds

S_{1}[i + 1]

S_{1}[i]
from INT_1:sch 7(L300, L400);

L902: f = (OnlinePackingHistory (a,(NextFit a))) . n by HL00, defPackHistory, L030;

thus n = card (Seg n) by FINSEQ_1:57

.= card (rng f) by L020, L030, L899, L902 ; :: thesis: verum

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)

let epsilon be Real; :: thesis: 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)

let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: 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)

let f be non empty FinSequence of NAT ; :: thesis: ( 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)) implies n = card (rng f) )

assume that

L010: n is odd and

L030: len a = n and

L040: epsilon = 1 / (n + 1) and

L050: 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 ) ) and

HL00: f = OnlinePacking (a,(NextFit a)) ; :: thesis: n = card (rng f)

L020: 1 <= n by L010, NF992;

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

defpred S

L300: S

proof

L400:
for i being Element of NAT st 1 <= i & i < len a & S
L305:
(OnlinePackingHistory (a,(NextFit a))) . 1 = <*1*>
by defPackHistory;

L324: 1 = (2 * 0) + 1 ;

L332: 1 in Seg n by L020;

SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . 1),{(((OnlinePackingHistory (a,(NextFit a))) . 1) . 1)}) = a . 1 by NF502

.= 2 * epsilon by L324, L332, L050 ;

hence S_{1}[1]
by L305, FINSEQ_1:def 8, FINSEQ_1:39, FINSEQ_1:2, L324; :: thesis: verum

end;L324: 1 = (2 * 0) + 1 ;

L332: 1 in Seg n by L020;

SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . 1),{(((OnlinePackingHistory (a,(NextFit a))) . 1) . 1)}) = a . 1 by NF502

.= 2 * epsilon by L324, L332, L050 ;

hence S

S

proof

L899:
for i being Element of NAT st 1 <= i & i <= len a holds
let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < len a & S_{1}[i0] implies S_{1}[i0 + 1] )

assume that

L410: 1 <= i0 and

L411: i0 < len a and

L412: S_{1}[i0]
; :: thesis: S_{1}[i0 + 1]

reconsider i0p = i0 + 1 as Nat ;

L469: 1 + 0 <= i0 + 1 by XREAL_1:7;

L480: i0p <= n by L411, L030, NAT_1:13;

then L490: i0p in Seg n by L469;

reconsider hi0 = (OnlinePackingHistory (a,(NextFit a))) . i0 as FinSequence of NAT by L410, L411, NF505;

reconsider hi0p = (OnlinePackingHistory (a,(NextFit a))) . i0p as FinSequence of NAT by L469, L030, L480, NF505;

L496: ( hi0p = hi0 ^ <*((NextFit a) . ((a . i0p),hi0))*> & hi0p . i0p = (NextFit a) . ((a . i0p),hi0) ) by L410, L411, NF520;

L498: len hi0 = i0 by L410, L411, NF510;

L500: ( i0p is odd implies ( hi0p . i0p = i0p & rng hi0p = Seg i0p & SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon ) )_{1}[i0 + 1]
by L500; :: thesis: verum

end;assume that

L410: 1 <= i0 and

L411: i0 < len a and

L412: S

reconsider i0p = i0 + 1 as Nat ;

L469: 1 + 0 <= i0 + 1 by XREAL_1:7;

L480: i0p <= n by L411, L030, NAT_1:13;

then L490: i0p in Seg n by L469;

reconsider hi0 = (OnlinePackingHistory (a,(NextFit a))) . i0 as FinSequence of NAT by L410, L411, NF505;

reconsider hi0p = (OnlinePackingHistory (a,(NextFit a))) . i0p as FinSequence of NAT by L469, L030, L480, NF505;

L496: ( hi0p = hi0 ^ <*((NextFit a) . ((a . i0p),hi0))*> & hi0p . i0p = (NextFit a) . ((a . i0p),hi0) ) by L410, L411, NF520;

L498: len hi0 = i0 by L410, L411, NF510;

L500: ( i0p is odd implies ( hi0p . i0p = i0p & rng hi0p = Seg i0p & SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon ) )

proof

( i0p is even implies ( hi0p . i0p = i0p & rng hi0p = Seg i0p & SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon ) )
assume L510:
i0p is odd
; :: thesis: ( hi0p . i0p = i0p & rng hi0p = Seg i0p & SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon )

then a . i0p = 2 * epsilon by L050, L490;

then L542: (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) = 1 + epsilon by L510, L412;

L549: 0 + 1 < epsilon + 1 by XREAL_1:139, L040, XREAL_1:6;

L580: hi0p . i0p = (NextFit a) . ((a . i0p),hi0) by L410, L411, NF520

.= (hi0 . i0) + 1 by L549, L542, L498, defNextFit ;

hence hi0p . i0p = i0p by L412; :: thesis: ( rng hi0p = Seg i0p & SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon )

thus rng hi0p = (rng hi0) \/ {(hi0p . i0p)} by L410, L411, NF525

.= Seg i0p by L580, L412, FINSEQ_1:9 ; :: thesis: SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon

not i0 + 1 in Seg i0 by XREAL_1:29, FINSEQ_1:1;

then L590: SumBin (a,hi0,{((hi0 . i0) + 1)}) = 0 by L412, ZFMISC_1:50, NF290;

SumBin (a,hi0p,{(hi0p . i0p)}) = (SumBin (a,hi0,{(hi0p . i0p)})) + (a . ((len hi0) + 1)) by L496, L498, L480, L030, NF200

.= a . (i0 + 1) by L580, L590, L410, L411, NF510

.= 2 * epsilon by L490, L510, L050 ;

hence SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon ; :: thesis: verum

end;then a . i0p = 2 * epsilon by L050, L490;

then L542: (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) = 1 + epsilon by L510, L412;

L549: 0 + 1 < epsilon + 1 by XREAL_1:139, L040, XREAL_1:6;

L580: hi0p . i0p = (NextFit a) . ((a . i0p),hi0) by L410, L411, NF520

.= (hi0 . i0) + 1 by L549, L542, L498, defNextFit ;

hence hi0p . i0p = i0p by L412; :: thesis: ( rng hi0p = Seg i0p & SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon )

thus rng hi0p = (rng hi0) \/ {(hi0p . i0p)} by L410, L411, NF525

.= Seg i0p by L580, L412, FINSEQ_1:9 ; :: thesis: SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon

not i0 + 1 in Seg i0 by XREAL_1:29, FINSEQ_1:1;

then L590: SumBin (a,hi0,{((hi0 . i0) + 1)}) = 0 by L412, ZFMISC_1:50, NF290;

SumBin (a,hi0p,{(hi0p . i0p)}) = (SumBin (a,hi0,{(hi0p . i0p)})) + (a . ((len hi0) + 1)) by L496, L498, L480, L030, NF200

.= a . (i0 + 1) by L580, L590, L410, L411, NF510

.= 2 * epsilon by L490, L510, L050 ;

hence SumBin (a,((OnlinePackingHistory (a,(NextFit a))) . i0p),{(((OnlinePackingHistory (a,(NextFit a))) . i0p) . i0p)}) = 2 * epsilon ; :: thesis: verum

proof

hence
S
assume L710:
i0p is even
; :: thesis: ( hi0p . i0p = i0p & rng hi0p = Seg i0p & SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon )

then L720: a . i0p = 1 - epsilon by L050, L490;

L742: (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) = 1 + epsilon by L720, L710, L412;

L749: 0 + 1 < epsilon + 1 by XREAL_1:139, L040, XREAL_1:6;

L780: hi0p . i0p = (NextFit a) . ((a . i0p),hi0) by L410, L411, NF520

.= (hi0 . i0) + 1 by L742, L498, defNextFit, L749 ;

hence hi0p . i0p = i0p by L412; :: thesis: ( rng hi0p = Seg i0p & SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon )

thus rng hi0p = (rng hi0) \/ {(hi0p . i0p)} by L410, L411, NF525

.= Seg i0p by L780, L412, FINSEQ_1:9 ; :: thesis: SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon

not i0 + 1 in Seg i0 by XREAL_1:29, FINSEQ_1:1;

then L790: SumBin (a,hi0,{((hi0 . i0) + 1)}) = 0 by L412, ZFMISC_1:50, NF290;

SumBin (a,hi0p,{(hi0p . i0p)}) = (SumBin (a,hi0,{(hi0p . i0p)})) + (a . ((len hi0) + 1)) by L496, L498, L480, L030, NF200

.= a . (i0 + 1) by L780, L790, L410, L411, NF510

.= 1 - epsilon by L490, L710, L050 ;

hence SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon ; :: thesis: verum

end;then L720: a . i0p = 1 - epsilon by L050, L490;

L742: (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) = 1 + epsilon by L720, L710, L412;

L749: 0 + 1 < epsilon + 1 by XREAL_1:139, L040, XREAL_1:6;

L780: hi0p . i0p = (NextFit a) . ((a . i0p),hi0) by L410, L411, NF520

.= (hi0 . i0) + 1 by L742, L498, defNextFit, L749 ;

hence hi0p . i0p = i0p by L412; :: thesis: ( rng hi0p = Seg i0p & SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon )

thus rng hi0p = (rng hi0) \/ {(hi0p . i0p)} by L410, L411, NF525

.= Seg i0p by L780, L412, FINSEQ_1:9 ; :: thesis: SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon

not i0 + 1 in Seg i0 by XREAL_1:29, FINSEQ_1:1;

then L790: SumBin (a,hi0,{((hi0 . i0) + 1)}) = 0 by L412, ZFMISC_1:50, NF290;

SumBin (a,hi0p,{(hi0p . i0p)}) = (SumBin (a,hi0,{(hi0p . i0p)})) + (a . ((len hi0) + 1)) by L496, L498, L480, L030, NF200

.= a . (i0 + 1) by L780, L790, L410, L411, NF510

.= 1 - epsilon by L490, L710, L050 ;

hence SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon ; :: thesis: verum

S

L902: f = (OnlinePackingHistory (a,(NextFit a))) . n by HL00, defPackHistory, L030;

thus n = card (Seg n) by FINSEQ_1:57

.= card (rng f) by L020, L030, L899, L902 ; :: thesis: verum