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
( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . 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
( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . 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
( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) ) )
assume L00: h = OnlinePackingHistory (a,Alg) ; :: thesis: for i being Nat st 1 <= i & i < len a holds
( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) )
let i be Nat; :: thesis: ( 1 <= i & i < len a implies ( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) ) )
assume L10: ( 1 <= i & i < len a ) ; :: thesis: ( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) )
consider d1 being Element of REAL , d2 being FinSequence of NAT such that
L20: ( d1 = a . (i + 1) & d2 = h . i ) and
L30: h . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> by L00, L10, defPackHistory;
thus h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> by L20, L30; :: thesis: (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i))
len (h . i) = i by L00, L10, NF510;
hence (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) by L20, L30, FINSEQ_1:42; :: thesis: verum