theorem Th4: :: EXTPRO_1:4

for i 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 s being State of S
for p being NAT -defined the InstructionsF of b₃ -valued Function
for k being Nat holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)