let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for l being Element of NAT
for f being FinPartState of S st l in dom f holds
(Shift f,k) . (l + k,S) = f . l
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for l being Element of NAT
for f being FinPartState of S st l in dom f holds
(Shift f,k) . (l + k,S) = f . l
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for l being Element of NAT
for f being FinPartState of S st l in dom f holds
(Shift f,k) . (l + k,S) = f . l
let l be Element of NAT ; :: thesis: for f being FinPartState of S st l in dom f holds
(Shift f,k) . (l + k,S) = f . l
let f be FinPartState of S; :: thesis: ( l in dom f implies (Shift f,k) . (l + k,S) = f . l )
assume A1: l in dom f ; :: thesis: (Shift f,k) . (l + k,S) = f . l
consider m being natural number such that
A2: l = il. S,m by AMISTD_1:26;
A3: m is Element of NAT by ORDINAL1:def 13;
thus (Shift f,k) . (l + k,S) = (Shift f,k) . (il. S,((locnum l,S) + k))
.= (Shift f,k) . (il. S,(m + k)) by A2, AMISTD_1:def 13
.= f . l by A1, A2, A3, Def16 ; :: thesis: verum