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_{1}[ Nat] means SumBin (a,(h . $1),{((h . $1) . $1)}) <= 1;

SumBin (a,(h . 1),{((h . 1) . 1)}) <= 1_{1}[1]
;

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

S_{1}[i + 1]

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

for i being Nat st 1 <= i & i <= len a holds

S_{1}[i]

SumBin (a,(h . i),{((h . i) . i)}) <= 1 ; :: thesis: verum

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

SumBin (a,(h . 1),{((h . 1) . 1)}) <= 1

proof

then L300:
S
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;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

L400: for i being Element of NAT st 1 <= i & i < 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

S_{1}[i0]
; :: thesis: S_{1}[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_{1}[i0 + 1]
; :: thesis: verum

end;assume that

L410: 1 <= i0 and

L411: i0 < len a and

S

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

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

end;

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

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;.= (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

S

for i being Nat st 1 <= i & i <= len a holds

S

proof

hence
for i being Nat st 1 <= i & i <= len a holds
let i be Nat; :: thesis: ( 1 <= i & i <= len a implies S_{1}[i] )

assume that

L910: 1 <= i and

L911: i <= len a ; :: thesis: S_{1}[i]

i in NAT by ORDINAL1:def 12;

hence S_{1}[i]
by L910, L911, L900; :: thesis: verum

end;assume that

L910: 1 <= i and

L911: i <= len a ; :: thesis: S

i in NAT by ORDINAL1:def 12;

hence S

SumBin (a,(h . i),{((h . i) . i)}) <= 1 ; :: thesis: verum