let s be State of SCMPDS ; :: 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 SCMPDS )
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 SCMPDS
then A1: CurInstr (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s)) = halt SCMPDS by AMI_1:def 46;
let k be Element of NAT ; :: thesis: ( LifeSpan (ProgramPart s),s <= k implies CurInstr (ProgramPart s),(Comput (ProgramPart s),s,k) = halt SCMPDS )
assume LifeSpan (ProgramPart s),s <= k ; :: thesis: CurInstr (ProgramPart s),(Comput (ProgramPart s),s,k) = halt SCMPDS
then Comput (ProgramPart s),s,(LifeSpan (ProgramPart s),s) = Comput (ProgramPart s),s,k by A1, AMI_1:52;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,k) = halt SCMPDS by A1; :: thesis: verum