theorem Th4: :: AMISTD_5:4

for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N
for INS being Instruction of S
for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)