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, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds

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

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds

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

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

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

defpred S_{1}[ Nat] means for j being Nat st j in rng (h . $1) holds

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

for j being Nat st j in rng (h . 1) holds

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

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

S_{1}[i0 + 1]

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

thus for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds

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

for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds

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

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds

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

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

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

defpred S

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

for j being Nat st j in rng (h . 1) holds

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

proof

then F1:
S
let j be Nat; :: thesis: ( j in rng (h . 1) implies SumBin (a,(h . 1),{j}) <= 1 )

assume FF000: j in rng (h . 1) ; :: thesis: SumBin (a,(h . 1),{j}) <= 1

FF005: 1 <= len a by NAT_1:14;

h . 1 = {[1,1]} by HN00, defPackHistory;

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

then FF020: j = 1 by FF000, TARSKI:def 1;

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

then (h . 1) . 1 = 1 by FINSEQ_1:def 8;

hence SumBin (a,(h . 1),{j}) <= 1 by FF005, HN00, NF880, FF020; :: thesis: verum

end;assume FF000: j in rng (h . 1) ; :: thesis: SumBin (a,(h . 1),{j}) <= 1

FF005: 1 <= len a by NAT_1:14;

h . 1 = {[1,1]} by HN00, defPackHistory;

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

then FF020: j = 1 by FF000, TARSKI:def 1;

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

then (h . 1) . 1 = 1 by FINSEQ_1:def 8;

hence SumBin (a,(h . 1),{j}) <= 1 by FF005, HN00, NF880, FF020; :: thesis: verum

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

F21: ( 1 <= i0 & i0 < len a ) and

F22: S_{1}[i0]
; :: thesis: S_{1}[i0 + 1]

set i0p = i0 + 1;

F26: i0 + 1 <= len a by F21, INT_1:7;

for j being Nat st j in rng (h . (i0 + 1)) holds

SumBin (a,(h . (i0 + 1)),{j}) <= 1_{1}[i0 + 1]
; :: thesis: verum

end;assume that

F21: ( 1 <= i0 & i0 < len a ) and

F22: S

set i0p = i0 + 1;

F26: i0 + 1 <= len a by F21, INT_1:7;

for j being Nat st j in rng (h . (i0 + 1)) holds

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

proof

hence
S
let j be Nat; :: thesis: ( j in rng (h . (i0 + 1)) implies SumBin (a,(h . (i0 + 1)),{j}) <= 1 )

assume I00: j in rng (h . (i0 + 1)) ; :: thesis: SumBin (a,(h . (i0 + 1)),{j}) <= 1

rng (h . (i0 + 1)) = (rng (h . i0)) \/ {((h . (i0 + 1)) . (i0 + 1))} by HN00, F21, NF525;

then rng (h . (i0 + 1)) = ((rng (h . i0)) \ {((h . (i0 + 1)) . (i0 + 1))}) \/ {((h . (i0 + 1)) . (i0 + 1))} by XBOOLE_1:39;

end;assume I00: j in rng (h . (i0 + 1)) ; :: thesis: SumBin (a,(h . (i0 + 1)),{j}) <= 1

rng (h . (i0 + 1)) = (rng (h . i0)) \/ {((h . (i0 + 1)) . (i0 + 1))} by HN00, F21, NF525;

then rng (h . (i0 + 1)) = ((rng (h . i0)) \ {((h . (i0 + 1)) . (i0 + 1))}) \/ {((h . (i0 + 1)) . (i0 + 1))} by XBOOLE_1:39;

per cases then
( j in (rng (h . i0)) \ {((h . (i0 + 1)) . (i0 + 1))} or j in {((h . (i0 + 1)) . (i0 + 1))} )
by I00, XBOOLE_0:def 3;

end;

suppose IA00:
j in (rng (h . i0)) \ {((h . (i0 + 1)) . (i0 + 1))}
; :: thesis: SumBin (a,(h . (i0 + 1)),{j}) <= 1

IA05:
j <> (h . (i0 + 1)) . (i0 + 1)
by IA00, ZFMISC_1:56;

IA09: ( h . (i0 + 1) = (h . i0) ^ <*((NextFit a) . ((a . (i0 + 1)),(h . i0)))*> & (h . (i0 + 1)) . (i0 + 1) = (NextFit a) . ((a . (i0 + 1)),(h . i0)) ) by HN00, F21, NF520;

set f = h . i0;

IA35: h . i0 is FinSequence of NAT by HN00, F21, NF505;

IA36: h . (i0 + 1) is FinSequence of NAT by HN00, XREAL_1:31, F26, NF505;

set b = (h . (i0 + 1)) . (i0 + 1);

SumBin (a,(h . (i0 + 1)),{j}) = SumBin (a,(h . i0),{j}) by IA09, IA05, IA35, IA36, NF110;

hence SumBin (a,(h . (i0 + 1)),{j}) <= 1 by IA00, F22; :: thesis: verum

end;IA09: ( h . (i0 + 1) = (h . i0) ^ <*((NextFit a) . ((a . (i0 + 1)),(h . i0)))*> & (h . (i0 + 1)) . (i0 + 1) = (NextFit a) . ((a . (i0 + 1)),(h . i0)) ) by HN00, F21, NF520;

set f = h . i0;

IA35: h . i0 is FinSequence of NAT by HN00, F21, NF505;

IA36: h . (i0 + 1) is FinSequence of NAT by HN00, XREAL_1:31, F26, NF505;

set b = (h . (i0 + 1)) . (i0 + 1);

SumBin (a,(h . (i0 + 1)),{j}) = SumBin (a,(h . i0),{j}) by IA09, IA05, IA35, IA36, NF110;

hence SumBin (a,(h . (i0 + 1)),{j}) <= 1 by IA00, F22; :: thesis: verum

S

thus for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds

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

proof

let i, j be Nat; :: thesis: ( 1 <= i & i <= len a & j in rng (h . i) implies SumBin (a,(h . i),{j}) <= 1 )

assume that

L910: ( 1 <= i & i <= len a ) and

L912: j in rng (h . i) ; :: thesis: SumBin (a,(h . i),{j}) <= 1

i in NAT by ORDINAL1:def 12;

hence SumBin (a,(h . i),{j}) <= 1 by L910, L900, L912; :: thesis: verum

end;assume that

L910: ( 1 <= i & i <= len a ) and

L912: j in rng (h . i) ; :: thesis: SumBin (a,(h . i),{j}) <= 1

i in NAT by ORDINAL1:def 12;

hence SumBin (a,(h . i),{j}) <= 1 by L910, L900, L912; :: thesis: verum