theorem Th5: :: AMISTD_5:5

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
for j, k being Nat st IC s = j + k holds
Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)