let s be State of SCM+FSA; :: thesis: ( ProgramPart s halts_on s implies for k being Element of NAT st LifeSpan ((ProgramPart s),s) <= k holds
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA )
assume ProgramPart s halts_on s ; :: thesis: for k being Element of NAT st LifeSpan ((ProgramPart s),s) <= k holds
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA
then A1: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s))))) = halt SCM+FSA by EXTPRO_1:def 14;
let k be Element of NAT ; :: thesis: ( LifeSpan ((ProgramPart s),s) <= k implies CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA )
set i = LifeSpan ((ProgramPart s),s);
assume LifeSpan ((ProgramPart s),s) <= k ; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA
then Comput ((ProgramPart s),s,k) = Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s),s))) by A1, EXTPRO_1:6;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA by A1; :: thesis: verum