theorem Th13: :: AMI_8:13

for n being Nat
for s being State of SCM
for P being Instruction-Sequence of SCM
for I being sequential Instruction of SCM st CurInstr (P,(Comput (P,s,n))) = I & IC (Comput (P,s,n)) in dom P holds
IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1