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
( ProgramPart s halts_on s & (Result (ProgramPart s),s) . (dl. aux) = term @ s & LifeSpan (ProgramPart s),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
( ProgramPart s halts_on s & (Result (ProgramPart s),s) . (dl. aux) = term @ s & LifeSpan (ProgramPart s),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 ( ProgramPart s halts_on s & (Result (ProgramPart s),s) . (dl. aux) = term @ s & LifeSpan (ProgramPart s),s = len (SCM-Compile term,aux) ) )
assume A1: aux > max_Data-Loc_in term ; :: thesis: ( ProgramPart s halts_on s & (Result (ProgramPart s),s) . (dl. aux) = term @ s & LifeSpan (ProgramPart s),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 = Comput (ProgramPart s),s,(i + 1) and
A3: i + 1 = len (SCM-Compile term,aux) and
A4: IC (Comput (ProgramPart s),s,i) = n + i and
A5: IC u = n + (i + 1) and
A6: u . (dl. aux) = term @ s and
for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) by A1, Th14;
len <%(halt SCM )%> = 1 by AFINSQ_1:38;
then len ((SCM-Compile term,aux) ^ <%(halt SCM )%>) = (i + 1) + 1 by A3, AFINSQ_1:20;
then i + 1 < len ((SCM-Compile term,aux) ^ <%(halt SCM )%>) by NAT_1:13;
then A7: s . (n + (i + 1)) = ((SCM-Compile term,aux) ^ <%(halt SCM )%>) . (i + 1) by SCM_1:def 1
.= halt SCM by A3, AFINSQ_1:40 ;
hence ProgramPart s halts_on s by A2, A5, SCM_1:3; :: thesis: ( (Result (ProgramPart s),s) . (dl. aux) = term @ s & LifeSpan (ProgramPart s),s = len (SCM-Compile term,aux) )
thus (Result (ProgramPart s),s) . (dl. aux) = term @ s by A2, A5, A6, A7, SCM_1:4; :: thesis: LifeSpan (ProgramPart s),s = len (SCM-Compile term,aux)
n + i <> n + (i + 1) ;
hence LifeSpan (ProgramPart s),s = len (SCM-Compile term,aux) by A2, A3, A4, A5, A7, SCM_1:17; :: thesis: verum