let a be non empty FinSequence of REAL ; :: thesis: for Alg being Function of [:REAL,(NAT *):],NAT

for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds

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

len (h . i) = i

let Alg be Function of [:REAL,(NAT *):],NAT; :: thesis: for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds

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

len (h . i) = i

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

len (h . i) = i )

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

len (h . i) = i

defpred S_{1}[ Nat] means len (h . $1) = $1;

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

then L05: S_{1}[1]
by FINSEQ_1:39;

L08: 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(L05, L08);

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

S_{1}[i]

len (h . i) = i ; :: thesis: verum

for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds

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

len (h . i) = i

let Alg be Function of [:REAL,(NAT *):],NAT; :: thesis: for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds

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

len (h . i) = i

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

len (h . i) = i )

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

len (h . i) = i

defpred S

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

then L05: S

L08: 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 im be Element of NAT ; :: thesis: ( 1 <= im & im < len a & S_{1}[im] implies S_{1}[im + 1] )

assume that

L10: ( 1 <= im & im < len a ) and

L15: len (h . im) = im ; :: thesis: S_{1}[im + 1]

consider d1 being Element of REAL , d2 being FinSequence of NAT such that

L20: ( d1 = a . (im + 1) & d2 = h . im ) and

L30: h . (im + 1) = d2 ^ <*(Alg . (d1,d2))*> by L00, L10, defPackHistory;

len (h . (im + 1)) = (len (h . im)) + (len <*(Alg . ((a . (im + 1)),(h . im)))*>) by L20, L30, FINSEQ_1:22

.= im + 1 by FINSEQ_1:39, L15 ;

hence S_{1}[im + 1]
; :: thesis: verum

end;assume that

L10: ( 1 <= im & im < len a ) and

L15: len (h . im) = im ; :: thesis: S

consider d1 being Element of REAL , d2 being FinSequence of NAT such that

L20: ( d1 = a . (im + 1) & d2 = h . im ) and

L30: h . (im + 1) = d2 ^ <*(Alg . (d1,d2))*> by L00, L10, defPackHistory;

len (h . (im + 1)) = (len (h . im)) + (len <*(Alg . ((a . (im + 1)),(h . im)))*>) by L20, L30, FINSEQ_1:22

.= im + 1 by FINSEQ_1:39, L15 ;

hence S

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

len (h . i) = i ; :: thesis: verum