theorem :: EXTPRO_1:6

for k being Nat
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))