theorem Th12: :: SCM_COMP:12

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)),n) c= F holds
for s being b₄ -started State of SCM st aux > max_Data-Loc_in term holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile (term,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = term @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )