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

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies 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 )

assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: 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

let i, k be Nat; :: thesis: ( 1 <= i & i < len a & rng (h . i) = Seg k & rng (h . (i + 1)) = Seg (k + 1) implies (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1 )

assume that

L060: 1 <= i and

L061: i < len a and

L062: rng (h . i) = Seg k and

L063: rng (h . (i + 1)) = Seg (k + 1) ; :: thesis: (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1

reconsider hi = h . i as FinSequence of NAT by HN00, L060, L061, NF505;

L030: hi <> {} by HN00, L060, L061, NF510;

L074: 1 + 0 <= i + 1 by XREAL_1:7;

L076: ip <= len a by L061, NAT_1:13;

reconsider hip = h . ip as FinSequence of NAT by HN00, L074, L076, NF505;

L080: hip = hi ^ <*((NextFit a) . ((a . ip),hi))*> by HN00, L060, L061, NF520;

L081: hip . ip = (NextFit a) . ((a . ip),hi) by HN00, L060, L061, NF520;

L100: ( ( (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) <= 1 implies (NextFit a) . ((a . ip),hi) = hi . (len hi) ) & ( (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) > 1 implies (NextFit a) . ((a . ip),hi) = (hi . (len hi)) + 1 ) ) by defNextFit;

len (h . ip) = ip by HN00, L074, L076, NF510;

then L540: (h . ip) . (len (h . ip)) = k + 1 by HN00, L074, L076, L063, NF807;

L559: len (hi ^ <*((hi . (len hi)) + 1)*>) = (len hi) + (len <*((hi . (len hi)) + 1)*>) by FINSEQ_1:22

.= (len hi) + 1 by FINSEQ_1:40 ;

L599: (h . ip) . (len (h . ip)) = (hi . (len hi)) + 1 by FINSEQ_1:42, L100, L499, L080, L559;

L649: len hi = ip - 1 by HN00, L060, L061, NF510;

L670: (len hi) + 1 <= len a by HN00, L060, L061, NF510, L076;

k + 1 <> k ;

then L700: SumBin (a,(h . ip),{k}) = SumBin (a,hi,{(hi . (len hi))}) by L100, L499, L080, L599, L540, NF110;

L799: SumBin (a,(hi ^ <*(k + 1)*>),{(k + 1)}) = (SumBin (a,hi,{(k + 1)})) + (a . ((len hi) + 1)) by L670, NF200;

0 <= SumBin (a,hi,{(k + 1)}) by NF280;

then ((a . ip) + (SumBin (a,hi,{(hi . (len hi))}))) + 0 <= ((a . ip) + (SumBin (a,hi,{(hi . (len hi))}))) + (SumBin (a,hi,{(k + 1)})) by XREAL_1:7;

hence (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1 by L499, L700, L799, L599, L540, L100, L080, L649, XXREAL_0:2; :: thesis: verum

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

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies 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 )

assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: 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

let i, k be Nat; :: thesis: ( 1 <= i & i < len a & rng (h . i) = Seg k & rng (h . (i + 1)) = Seg (k + 1) implies (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1 )

assume that

L060: 1 <= i and

L061: i < len a and

L062: rng (h . i) = Seg k and

L063: rng (h . (i + 1)) = Seg (k + 1) ; :: thesis: (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1

reconsider hi = h . i as FinSequence of NAT by HN00, L060, L061, NF505;

L030: hi <> {} by HN00, L060, L061, NF510;

L013: now :: thesis: 1 <= k

reconsider ip = i + 1 as Element of NAT by ORDINAL1:def 12;assume
not 1 <= k
; :: thesis: contradiction

then k < 0 + 1 ;

then k <= 0 by NAT_1:13;

hence contradiction by L062, L030; :: thesis: verum

end;then k < 0 + 1 ;

then k <= 0 by NAT_1:13;

hence contradiction by L062, L030; :: thesis: verum

L074: 1 + 0 <= i + 1 by XREAL_1:7;

L076: ip <= len a by L061, NAT_1:13;

reconsider hip = h . ip as FinSequence of NAT by HN00, L074, L076, NF505;

L080: hip = hi ^ <*((NextFit a) . ((a . ip),hi))*> by HN00, L060, L061, NF520;

L081: hip . ip = (NextFit a) . ((a . ip),hi) by HN00, L060, L061, NF520;

L100: ( ( (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) <= 1 implies (NextFit a) . ((a . ip),hi) = hi . (len hi) ) & ( (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) > 1 implies (NextFit a) . ((a . ip),hi) = (hi . (len hi)) + 1 ) ) by defNextFit;

L499: now :: thesis: (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) > 1

reconsider kp = k + 1 as Nat ;assume
not (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) > 1
; :: thesis: contradiction

then L140: hip . ip = hi . (len hi) by L081, defNextFit

.= hi . i by HN00, L060, L061, NF510

.= k by HN00, L060, L061, L062, NF807 ;

L149: k in Seg k by L013;

rng (h . (i + 1)) = (rng (h . i)) \/ {k} by HN00, L060, L061, NF525, L140

.= Seg k by L062, L149, ZFMISC_1:31, XBOOLE_1:12 ;

then k = k + 1 by L063, FINSEQ_1:6;

hence contradiction ; :: thesis: verum

end;then L140: hip . ip = hi . (len hi) by L081, defNextFit

.= hi . i by HN00, L060, L061, NF510

.= k by HN00, L060, L061, L062, NF807 ;

L149: k in Seg k by L013;

rng (h . (i + 1)) = (rng (h . i)) \/ {k} by HN00, L060, L061, NF525, L140

.= Seg k by L062, L149, ZFMISC_1:31, XBOOLE_1:12 ;

then k = k + 1 by L063, FINSEQ_1:6;

hence contradiction ; :: thesis: verum

len (h . ip) = ip by HN00, L074, L076, NF510;

then L540: (h . ip) . (len (h . ip)) = k + 1 by HN00, L074, L076, L063, NF807;

L559: len (hi ^ <*((hi . (len hi)) + 1)*>) = (len hi) + (len <*((hi . (len hi)) + 1)*>) by FINSEQ_1:22

.= (len hi) + 1 by FINSEQ_1:40 ;

L599: (h . ip) . (len (h . ip)) = (hi . (len hi)) + 1 by FINSEQ_1:42, L100, L499, L080, L559;

L649: len hi = ip - 1 by HN00, L060, L061, NF510;

L670: (len hi) + 1 <= len a by HN00, L060, L061, NF510, L076;

k + 1 <> k ;

then L700: SumBin (a,(h . ip),{k}) = SumBin (a,hi,{(hi . (len hi))}) by L100, L499, L080, L599, L540, NF110;

L799: SumBin (a,(hi ^ <*(k + 1)*>),{(k + 1)}) = (SumBin (a,hi,{(k + 1)})) + (a . ((len hi) + 1)) by L670, NF200;

0 <= SumBin (a,hi,{(k + 1)}) by NF280;

then ((a . ip) + (SumBin (a,hi,{(hi . (len hi))}))) + 0 <= ((a . ip) + (SumBin (a,hi,{(hi . (len hi))}))) + (SumBin (a,hi,{(k + 1)})) by XREAL_1:7;

hence (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1 by L499, L700, L799, L599, L540, L100, L080, L649, XXREAL_0:2; :: thesis: verum