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_{3} -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_{2} -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

for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds

for s being b

( 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

( 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