theorem :: SCM_1:14

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(halt SCM)%> c= F holds
for s being 0 -started State-consisting of <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )