theorem Th11: :: SCM_1:11

for F being NAT -defined the InstructionsF of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for a being Data-Location
for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds
( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )