theorem :: SCM_1:15

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of <%i1,i2%> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )