theorem :: SCM_1:17

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(SubFrom ((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) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )