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)) ^ <%(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)) )
let term be bin-term; :: thesis: 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)) )
let aux, n be Element of NAT ; :: thesis: ( Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),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)) ^ <%(halt SCM)%>),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 A1, AFINSQ_1:82;
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 A2, Th12;
len <%(halt SCM)%> = 1 by AFINSQ_1:34;
then len ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) = (i + 1) + 1 by A4, AFINSQ_1:17;
then i + 1 < len ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) by NAT_1:13;
then i + 1 in dom ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) by AFINSQ_1:86;
then A8: F . (n + (i + 1)) = ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) . (i + 1) by A1, VALUED_1:51
.= halt SCM by A4, AFINSQ_1:36 ;
hence F halts_on s by A3, A6, EXTPRO_1:30; :: 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 A3, A6, A7, A8, EXTPRO_1:7; :: thesis: LifeSpan (F,s) = len (SCM-Compile (term,aux))
n + i <> n + (i + 1) ;
hence LifeSpan (F,s) = len (SCM-Compile (term,aux)) by A3, A4, A5, A6, A8, EXTPRO_1:33; :: thesis: verum