theorem Th1: :: SCMPDS_9:1

for i being Instruction of SCMPDS
for l being Element of NAT st ( for s being State of SCMPDS st IC s = l holds
(Exec (i,s)) . (IC ) = (IC s) + 1 ) holds
NIC (i,l) = {(l + 1)}