let a be non empty FinSequence of REAL ; 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 * ; ( 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))
; 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 S1[ 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:
S1[1]
by L219, FINSEQ_1:2, L289, FINSEQ_1:def 8;
L400:
for i being Element of NAT st 1 <= i & i < len a & S1[i] holds
S1[i + 1]
proof
let i0 be
Element of
NAT ;
( 1 <= i0 & i0 < len a & S1[i0] implies S1[i0 + 1] )
assume that L410:
1
<= i0
and L411:
i0 < len a
and L412:
S1[
i0]
;
S1[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 )
proof
per cases
( (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1 or (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1 )
;
suppose L500:
(a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1
;
ex k being Nat st
( 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;
verum end; suppose L700:
(a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1
;
ex k being Nat st
( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )then L739:
k0 in Seg k0
;
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;
verum end; end;
end;
hence
S1[
i0 + 1]
;
verum
end;
L800:
for i being Element of NAT st 1 <= i & i <= len a holds
S1[i]
from INT_1:sch 7(L300, L400);
for i being Nat st 1 <= i & i <= len a holds
S1[i]
hence
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 )
; verum