let term be bin-term; :: thesis: for aux, n, k being Element of NAT
for s being State-consisting of n,n,k,(SCM-Compile term,aux) ^ <*(halt SCM )*>, <*> INT st aux > max_Data-Loc_in term holds
( s is halting & (Result s) . (dl. aux) = term @ s & LifeSpan s = len (SCM-Compile term,aux) )
let aux, n, k be Element of NAT ; :: thesis: for s being State-consisting of n,n,k,(SCM-Compile term,aux) ^ <*(halt SCM )*>, <*> INT st aux > max_Data-Loc_in term holds
( s is halting & (Result s) . (dl. aux) = term @ s & LifeSpan s = len (SCM-Compile term,aux) )
let s be State-consisting of n,n,k,(SCM-Compile term,aux) ^ <*(halt SCM )*>, <*> INT ; :: thesis: ( aux > max_Data-Loc_in term implies ( s is halting & (Result s) . (dl. aux) = term @ s & LifeSpan s = len (SCM-Compile term,aux) ) )
assume A1: aux > max_Data-Loc_in term ; :: thesis: ( s is halting & (Result s) . (dl. aux) = term @ s & LifeSpan s = len (SCM-Compile term,aux) )
s is State-consisting of n,n,k, SCM-Compile term,aux, <*> INT by Th1;
then consider i being Element of NAT , u being State of SCM such that
A2: ( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile term,aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (n + (i + 1)) & u . (dl. aux) = term @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) by A1, Th14;
len <*(halt SCM )*> = 1 by FINSEQ_1:57;
then len ((SCM-Compile term,aux) ^ <*(halt SCM )*>) = (i + 1) + 1 by A2, FINSEQ_1:35;
then i + 1 < len ((SCM-Compile term,aux) ^ <*(halt SCM )*>) by NAT_1:13;
then A3: s . (il. (n + (i + 1))) = ((SCM-Compile term,aux) ^ <*(halt SCM )*>) . ((i + 1) + 1) by SCM_1:def 1
.= halt SCM by A2, FINSEQ_1:59 ;
hence s is halting by A2, SCM_1:3; :: thesis: ( (Result s) . (dl. aux) = term @ s & LifeSpan s = len (SCM-Compile term,aux) )
thus (Result s) . (dl. aux) = term @ s by A2, A3, SCM_1:4; :: thesis: LifeSpan s = len (SCM-Compile term,aux)
( il. (n + i) <> il. (n + (i + 1)) & (n + i) + 1 = n + (i + 1) ) ;
hence LifeSpan s = len (SCM-Compile term,aux) by A2, A3, SCM_1:17; :: thesis: verum