let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: for term being bin-term
for aux, n, k being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds
for s being b₃ -started State-consisting of k, <*> INT 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, k being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds
for s being b₂ -started State-consisting of k, <*> INT 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, k be Element of NAT ; :: thesis: ( Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F implies for s being n -started State-consisting of k, <*> INT 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 ZZ: Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F ; :: thesis: for s being n -started State-consisting of k, <*> INT 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-consisting of k, <*> INT; :: 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 A1: 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 ZZ, AFINSQ_1:86;
then consider i being Element of NAT , u being State of SCM such that
A2: u = Comput (F,s,(i + 1)) and
A3: i + 1 = len (SCM-Compile (term,aux)) and
A4: IC (Comput (F,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 i + 1 in dom ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) by NAT_1:45;
then A7: F . (n + (i + 1)) = ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) . (i + 1) by ZZ, PBOOLE:159
.= halt SCM by A3, AFINSQ_1:40 ;
hence F halts_on s by A2, A5, EXTPRO_1:31; :: 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 A2, A5, A6, A7, EXTPRO_1:32; :: thesis: LifeSpan (F,s) = len (SCM-Compile (term,aux))
n + i <> n + (i + 1) ;
hence LifeSpan (F,s) = len (SCM-Compile (term,aux)) by A2, A3, A4, A5, A7, EXTPRO_1:34; :: thesis: verum