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

proof

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;

then L100: S₁[1] ;
L400: for i0 being Element of NAT st 1 <= i0 & i0 < len a & S₁[i0] holds
S₁[i0 + 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]
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

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

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

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;

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 ;

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

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;

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

hence (SumBin (a,(h . (i0 + 1)),{l})) + (SumBin (a,(h . (i0 + 1)),{(l + 1)})) > 1 by HN00, L410, L411, L427, L600, L430, NF815; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

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

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;