theorem :: AMISTD_2:11

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Nat holds Comput (P,s,n) = s