let a be non empty 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

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k )

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

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k ) )

assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i being Nat st 1 <= i & i <= len a holds

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k )

defpred S_{1}[ Nat] means ex k being Nat st

( rng (h . $1) = Seg k & (h . $1) . $1 = k );

(OnlinePackingHistory (a,(NextFit a))) . 1 = {[1,1]} by defPackHistory;

then L219: rng (h . 1) = {1} by HN00, RELAT_1:9;

L289: h . 1 = <*1*> by defPackHistory, HN00;

L300: S_{1}[1]
by L219, FINSEQ_1:2, L289, FINSEQ_1:def 8;

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]

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k ) ; :: thesis: verum

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

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k )

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

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k ) )

assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i being Nat st 1 <= i & i <= len a holds

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k )

defpred S

( rng (h . $1) = Seg k & (h . $1) . $1 = k );

(OnlinePackingHistory (a,(NextFit a))) . 1 = {[1,1]} by defPackHistory;

then L219: rng (h . 1) = {1} by HN00, RELAT_1:9;

L289: h . 1 = <*1*> by defPackHistory, HN00;

L300: S

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

S

proof

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

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

L090: len (h . i0) = i0 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;

ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )_{1}[i0 + 1]
; :: thesis: verum

end;assume that

L410: 1 <= i0 and

L411: i0 < len a and

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

L090: len (h . i0) = i0 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;

ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

proof
end;

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

end;

suppose L500:
(a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1
; :: thesis: ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

rng hi0p = (Seg k0) \/ {(hi0p . i0p)}
by HN00, L410, L411, NF525, L427;

then rng hi0p = (Seg k0) \/ {(k0 + 1)} by HN00, L410, L411, NF520, L100, L500, L428

.= Seg (k0 + 1) by FINSEQ_1:9 ;

hence ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k ) by HN00, L410, L411, NF520, L100, L500, L428; :: thesis: verum

end;then rng hi0p = (Seg k0) \/ {(k0 + 1)} by HN00, L410, L411, NF520, L100, L500, L428

.= Seg (k0 + 1) by FINSEQ_1:9 ;

hence ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k ) by HN00, L410, L411, NF520, L100, L500, L428; :: thesis: verum

suppose L700:
(a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1
; :: thesis: ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

rng hi0p = (rng hi0) \/ {(hi0p . i0p)} by HN00, L410, L411, NF525

.= (Seg k0) \/ {k0} by L427, HN00, L410, L411, NF520, L100, L700, L428

.= Seg k0 by L739, ZFMISC_1:31, XBOOLE_1:12 ;

hence ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k ) by HN00, L410, L411, NF520, L100, L700, L428; :: thesis: verum

end;

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

now :: thesis: 1 <= k0

then L739:
k0 in Seg k0
;assume
not 1 <= k0
; :: thesis: contradiction

then k0 < 0 + 1 ;

then k0 <= 0 by NAT_1:13;

then hi0 = {} by L427;

hence contradiction by HN00, L410, L411, NF510; :: thesis: verum

end;then k0 < 0 + 1 ;

then k0 <= 0 by NAT_1:13;

then hi0 = {} by L427;

hence contradiction by HN00, L410, L411, NF510; :: thesis: verum

rng hi0p = (rng hi0) \/ {(hi0p . i0p)} by HN00, L410, L411, NF525

.= (Seg k0) \/ {k0} by L427, HN00, L410, L411, NF520, L100, L700, L428

.= Seg k0 by L739, ZFMISC_1:31, XBOOLE_1:12 ;

hence ex k being Nat st

( rng (h . i0p) = Seg k & (h . i0p) . i0p = k ) by HN00, L410, L411, NF520, L100, L700, L428; :: 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

L810: 1 <= i and

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

i in NAT by ORDINAL1:def 12;

hence S_{1}[i]
by L810, L811, L800; :: thesis: verum

end;assume that

L810: 1 <= i and

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

i in NAT by ORDINAL1:def 12;

hence S

ex k being Nat st

( rng (h . i) = Seg k & (h . i) . i = k ) ; :: thesis: verum