theorem :: SCM_1:20

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