for F being Instruction-Sequence of SCM
for term being bin-term
for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds
for s being b₄ -started State of SCM st aux > max_Data-Loc_in term holds
( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )