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

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

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

defpred S_{1}[ Nat] means for l, k being Nat st rng (h . $1) = Seg k & 2 <= k & 1 <= l & l < k holds

(SumBin (a,(h . $1),{l})) + (SumBin (a,(h . $1),{(l + 1)})) > 1;

for l, k being Nat st rng (h . 1) = Seg k & 2 <= k & 1 <= l & l < k holds

(SumBin (a,(h . 1),{l})) + (SumBin (a,(h . 1),{(l + 1)})) > 1_{1}[1]
;

L400: for i0 being Element of NAT st 1 <= i0 & i0 < len a & S_{1}[i0] holds

S_{1}[i0 + 1]

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

thus 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 :: thesis: verum

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

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

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

defpred S

(SumBin (a,(h . $1),{l})) + (SumBin (a,(h . $1),{(l + 1)})) > 1;

for l, k being Nat st rng (h . 1) = Seg k & 2 <= k & 1 <= l & l < k holds

(SumBin (a,(h . 1),{l})) + (SumBin (a,(h . 1),{(l + 1)})) > 1

proof

then L100:
S
let l, k be Nat; :: thesis: ( rng (h . 1) = Seg k & 2 <= k & 1 <= l & l < k implies (SumBin (a,(h . 1),{l})) + (SumBin (a,(h . 1),{(l + 1)})) > 1 )

assume that

L110: rng (h . 1) = Seg k and

L111: 2 <= k and

( 1 <= l & l < k ) ; :: thesis: (SumBin (a,(h . 1),{l})) + (SumBin (a,(h . 1),{(l + 1)})) > 1

Seg k = rng <*1*> by L110, HN00, defPackHistory

.= {1} by FINSEQ_1:38 ;

then k = 1 by FINSEQ_3:20;

hence (SumBin (a,(h . 1),{l})) + (SumBin (a,(h . 1),{(l + 1)})) > 1 by L111; :: thesis: verum

end;assume that

L110: rng (h . 1) = Seg k and

L111: 2 <= k and

( 1 <= l & l < k ) ; :: thesis: (SumBin (a,(h . 1),{l})) + (SumBin (a,(h . 1),{(l + 1)})) > 1

Seg k = rng <*1*> by L110, HN00, defPackHistory

.= {1} by FINSEQ_1:38 ;

then k = 1 by FINSEQ_3:20;

hence (SumBin (a,(h . 1),{l})) + (SumBin (a,(h . 1),{(l + 1)})) > 1 by L111; :: thesis: verum

L400: for i0 being Element of NAT st 1 <= i0 & i0 < len a & S

S

proof

L900:
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]

ex k being Nat st

( rng (h . i0) = Seg k & (h . i0) . i0 = k ) by HN00, L410, L411, NF805;

then consider k being Nat such that

L427: rng (h . i0) = Seg k ;

for l, k being Nat st rng (h . (i0 + 1)) = Seg k & 2 <= k & 1 <= l & l < k holds

(SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1_{1}[i0 + 1]
; :: thesis: verum

end;assume that

L410: 1 <= i0 and

L411: i0 < len a and

L412: S

ex k being Nat st

( rng (h . i0) = Seg k & (h . i0) . i0 = k ) by HN00, L410, L411, NF805;

then consider k being Nat such that

L427: rng (h . i0) = Seg k ;

for l, k being Nat st rng (h . (i0 + 1)) = Seg k & 2 <= k & 1 <= l & l < k holds

(SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1

proof

hence
S
let l, kp be Nat; :: thesis: ( rng (h . (i0 + 1)) = Seg kp & 2 <= kp & 1 <= l & l < kp implies (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1 )

assume that

L430: rng (h . (i0 + 1)) = Seg kp and

L431: 2 <= kp and

L432: 1 <= l and

L433: l < kp ; :: thesis: (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1

I20: rng (h . (i0 + 1)) = (rng (h . i0)) \/ {((h . (i0 + 1)) . (i0 + 1))} by HN00, L410, L411, NF525;

set f = (h . (i0 + 1)) . (i0 + 1);

end;assume that

L430: rng (h . (i0 + 1)) = Seg kp and

L431: 2 <= kp and

L432: 1 <= l and

L433: l < kp ; :: thesis: (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1

I20: rng (h . (i0 + 1)) = (rng (h . i0)) \/ {((h . (i0 + 1)) . (i0 + 1))} by HN00, L410, L411, NF525;

set f = (h . (i0 + 1)) . (i0 + 1);

per cases
( kp = k or kp = k + 1 )
by L427, L430, I20, NF600;

end;

suppose
kp = k
; :: thesis: (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1

then L540:
(SumBin (a,(h . i0),{l})) + (SumBin (a,(h . i0),{(l + 1)})) > 1
by L427, L431, L432, L433, L412;

L550: SumBin (a,(h . i0),{l}) <= SumBin (a,(h . (i0 + 1)),{l}) by HN00, L410, L411, NF530;

SumBin (a,(h . i0),{(l + 1)}) <= SumBin (a,(h . (i0 + 1)),{(l + 1)}) by HN00, L410, L411, NF530;

then (SumBin (a,(h . i0),{l})) + (SumBin (a,(h . i0),{(l + 1)})) <= (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) by L550, XREAL_1:7;

hence (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1 by L540, XXREAL_0:2; :: thesis: verum

end;L550: SumBin (a,(h . i0),{l}) <= SumBin (a,(h . (i0 + 1)),{l}) by HN00, L410, L411, NF530;

SumBin (a,(h . i0),{(l + 1)}) <= SumBin (a,(h . (i0 + 1)),{(l + 1)}) by HN00, L410, L411, NF530;

then (SumBin (a,(h . i0),{l})) + (SumBin (a,(h . i0),{(l + 1)})) <= (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) by L550, XREAL_1:7;

hence (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1 by L540, XXREAL_0:2; :: thesis: verum

suppose L600:
kp = k + 1
; :: thesis: (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1

set jay = kp - 2;

2 - 2 <= kp - 2 by L431, XREAL_1:9;

then kp - 2 in NAT by INT_1:3;

then reconsider jay = kp - 2 as Nat ;

l + 1 <= kp by L433, NAT_1:13;

then (l + 1) - 1 <= kp - 1 by XREAL_1:9;

then l <= jay + 1 ;

end;2 - 2 <= kp - 2 by L431, XREAL_1:9;

then kp - 2 in NAT by INT_1:3;

then reconsider jay = kp - 2 as Nat ;

l + 1 <= kp by L433, NAT_1:13;

then (l + 1) - 1 <= kp - 1 by XREAL_1:9;

then l <= jay + 1 ;

per cases then
( l <= kp - 2 or l = kp - 1 )
by NAT_1:8;

end;

suppose L700:
l <= kp - 2
; :: thesis: (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1

1 <= kp - 2
by L432, L700, XXREAL_0:2;

then L709: 1 + 1 <= ((k + 1) - 2) + 1 by XREAL_1:6, L600;

0 + l < 1 + ((k + 1) - 2) by L600, L700, XREAL_1:8;

then L740: (SumBin (a,(h . i0),{l})) + (SumBin (a,(h . i0),{(l + 1)})) > 1 by L427, L709, L432, L412;

L750: SumBin (a,(h . i0),{l}) <= SumBin (a,(h . (i0 + 1)),{l}) by HN00, L410, L411, NF530;

SumBin (a,(h . i0),{(l + 1)}) <= SumBin (a,(h . (i0 + 1)),{(l + 1)}) by HN00, L410, L411, NF530;

then (SumBin (a,(h . i0),{l})) + (SumBin (a,(h . i0),{(l + 1)})) <= (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) by L750, XREAL_1:7;

hence (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1 by L740, XXREAL_0:2; :: thesis: verum

end;then L709: 1 + 1 <= ((k + 1) - 2) + 1 by XREAL_1:6, L600;

0 + l < 1 + ((k + 1) - 2) by L600, L700, XREAL_1:8;

then L740: (SumBin (a,(h . i0),{l})) + (SumBin (a,(h . i0),{(l + 1)})) > 1 by L427, L709, L432, L412;

L750: SumBin (a,(h . i0),{l}) <= SumBin (a,(h . (i0 + 1)),{l}) by HN00, L410, L411, NF530;

SumBin (a,(h . i0),{(l + 1)}) <= SumBin (a,(h . (i0 + 1)),{(l + 1)}) by HN00, L410, L411, NF530;

then (SumBin (a,(h . i0),{l})) + (SumBin (a,(h . i0),{(l + 1)})) <= (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) by L750, XREAL_1:7;

hence (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1 by L740, XXREAL_0:2; :: thesis: verum

S

thus 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 :: thesis: verum

proof

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

assume that

L910: ( 1 <= i & i <= len a ) and

L911: ( rng (h . i) = Seg k & 2 <= k & 1 <= l & l < k ) ; :: thesis: (SumBin (a,(h . i),{l})) + (SumBin (a,(h . i),{(l + 1)})) > 1

i in NAT by ORDINAL1:def 12;

hence (SumBin (a,(h . i),{l})) + (SumBin (a,(h . i),{(l + 1)})) > 1 by L910, L900, L911; :: thesis: verum

end;assume that

L910: ( 1 <= i & i <= len a ) and

L911: ( rng (h . i) = Seg k & 2 <= k & 1 <= l & l < k ) ; :: thesis: (SumBin (a,(h . i),{l})) + (SumBin (a,(h . i),{(l + 1)})) > 1

i in NAT by ORDINAL1:def 12;

hence (SumBin (a,(h . i),{l})) + (SumBin (a,(h . i),{(l + 1)})) > 1 by L910, L900, L911; :: thesis: verum