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₁[ 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]

proof

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] by L305, FINSEQ_1:39, FINSEQ_1:2, L324; :: thesis: verum

end;

L400: for i being Element of NAT st 1 <= i & i < len a & S₁[i] holds
S₁[i + 1]

proof

let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < len a & S₁[i0] implies S₁[i0 + 1] )
assume that
L410: 1 <= i0 and
L411: i0 < len a and
L412: S₁[i0] ; :: thesis: S₁[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 ) )

proof

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;

( i0p is even implies ( hi0p . i0p = i0p & rng hi0p = Seg i0p & SumBin (a,hi0p,{(hi0p . i0p)}) = 1 - epsilon ) )

proof

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;

hence S₁[i0 + 1] by L500; :: thesis: verum

end;

L899: for i being Element of NAT st 1 <= i & i <= len a holds
S₁[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