let F be Instruction-Sequence of SCM; :: thesis: 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 b3 -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)) )

let term be bin-term; :: thesis: for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%()%>),n) c= F holds
for s being b2 -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)) )

let aux, n be Element of NAT ; :: thesis: ( Shift (((SCM-Compile (term,aux)) ^ <%()%>),n) c= F implies for s being n -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)) ) )

assume A1: Shift (((SCM-Compile (term,aux)) ^ <%()%>),n) c= F ; :: thesis: for s being n -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)) )

let s be n -started State of SCM; :: thesis: ( aux > max_Data-Loc_in term implies ( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) ) )
assume A2: aux > max_Data-Loc_in term ; :: thesis: ( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
Shift ((SCM-Compile (term,aux)),n) c= F by ;
then consider i being Element of NAT , u being State of SCM such that
A3: u = Comput (F,s,(i + 1)) and
A4: i + 1 = len (SCM-Compile (term,aux)) and
A5: IC (Comput (F,s,i)) = n + i and
A6: IC u = n + (i + 1) and
A7: u . (dl. aux) = term @ s and
for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) by ;
len <%()%> = 1 by AFINSQ_1:34;
then len ((SCM-Compile (term,aux)) ^ <%()%>) = (i + 1) + 1 by ;
then i + 1 < len ((SCM-Compile (term,aux)) ^ <%()%>) by NAT_1:13;
then i + 1 in dom ((SCM-Compile (term,aux)) ^ <%()%>) by AFINSQ_1:86;
then A8: F . (n + (i + 1)) = ((SCM-Compile (term,aux)) ^ <%()%>) . (i + 1) by
.= halt SCM by ;
hence F halts_on s by ; :: thesis: ( (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
thus (Result (F,s)) . (dl. aux) = term @ s by ; :: thesis: LifeSpan (F,s) = len (SCM-Compile (term,aux))
n + i <> n + (i + 1) ;
hence LifeSpan (F,s) = len (SCM-Compile (term,aux)) by ; :: thesis: verum