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 being Nat st 1 <= i & i <= len a holds
SumBin (a,(h . i),{((h . i) . i)}) <= 1
let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies for i being Nat st 1 <= i & i <= len a holds
SumBin (a,(h . i),{((h . i) . i)}) <= 1 )
assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i being Nat st 1 <= i & i <= len a holds
SumBin (a,(h . i),{((h . i) . i)}) <= 1
defpred S₁[ Nat] means SumBin (a,(h . $1),{((h . $1) . $1)}) <= 1;
SumBin (a,(h . 1),{((h . 1) . 1)}) <= 1

proof

L005: 1 <= len a by NAT_1:14;
L060: SumBin (a,(h . 1),{((h . 1) . 1)}) = a . 1 by HN00, NF502;
a is at_most_one ;
hence SumBin (a,(h . 1),{((h . 1) . 1)}) <= 1 by L005, L060; :: thesis: verum

end;

then L300: S₁[1] ;
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
S₁[i0] ; :: thesis: S₁[i0 + 1]
reconsider hi0 = h . i0 as FinSequence of NAT by HN00, L410, L411, NF505;
reconsider i0p = i0 + 1 as Element of NAT by ORDINAL1:def 12;
L074: 1 + 0 <= i0 + 1 by XREAL_1:7;
L076: i0p <= len a by L411, NAT_1:13;
reconsider hi0p = h . i0p as FinSequence of NAT by HN00, L074, L076, NF505;
consider k0 being Nat such that
L427: rng hi0 = Seg k0 and
L428: (h . i0) . i0 = k0 by HN00, L410, L411, NF805;
L080: hi0p = hi0 ^ <*((NextFit a) . ((a . i0p),hi0))*> by HN00, L410, L411, NF520;
L081: hi0p . i0p = (NextFit a) . ((a . i0p),hi0) by HN00, L410, L411, NF520;
L090: len (h . i0) = i0 by HN00, L410, L411, NF510;
L094: (len hi0) + 1 = i0p by HN00, L410, L411, NF510;
L100: ( ( (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1 implies (NextFit a) . ((a . i0p),hi0) = hi0 . i0 ) & ( (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1 implies (NextFit a) . ((a . i0p),hi0) = (hi0 . i0) + 1 ) ) by L090, defNextFit;
SumBin (a,(h . i0p),{((h . i0p) . i0p)}) <= 1

proof

per cases ( (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1 or (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1 ) ;

suppose (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1 ; :: thesis: SumBin (a,(h . i0p),{((h . i0p) . i0p)}) <= 1

L599: SumBin (a,(hi0 ^ <*(hi0p . i0p)*>),{(hi0p . i0p)}) = (SumBin (a,hi0,{(hi0p . i0p)})) + (a . ((len hi0) + 1)) by L094, L076, NF200;
not k0 + 1 in Seg k0 by XREAL_1:29, FINSEQ_1:1;
then L619: SumBin (a,hi0,{((hi0 . i0) + 1)}) = 0 by L427, L428, ZFMISC_1:50, NF290;
a is at_most_one ;
hence SumBin (a,(h . i0p),{((h . i0p) . i0p)}) <= 1 by L619, L100, L081, L599, L080, L074, L076, L094; :: thesis: verum

end;

suppose L700: (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1 ; :: thesis: SumBin (a,(h . i0p),{((h . i0p) . i0p)}) <= 1

SumBin (a,hi0p,{(hi0p . i0p)}) = (SumBin (a,hi0,{(hi0p . i0p)})) + (a . ((len hi0) + 1)) by L094, L076, NF200, L080, L081
.= (SumBin (a,hi0,{(hi0 . i0)})) + (a . i0p) by L090, defNextFit, L700, L081 ;
hence SumBin (a,(h . i0p),{((h . i0p) . i0p)}) <= 1 by L700; :: thesis: verum

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(L300, L400);
for i being Nat st 1 <= i & i <= len a holds
S₁[i]

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len a implies S₁[i] )
assume that
L910: 1 <= i and
L911: i <= len a ; :: thesis: S₁[i]
i in NAT by ORDINAL1:def 12;
hence S₁[i] by L910, L911, L900; :: thesis: verum

end;

hence for i being Nat st 1 <= i & i <= len a holds
SumBin (a,(h . i),{((h . i) . i)}) <= 1 ; :: thesis: verum