let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being State of SCMPDS st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt SCMPDS
let s be State of SCMPDS; :: thesis: ( P halts_on s implies for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt SCMPDS )
assume P halts_on s ; :: thesis: for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt SCMPDS
then A1: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt SCMPDS by EXTPRO_1:def 14;
let k be Element of NAT ; :: thesis: ( LifeSpan (P,s) <= k implies CurInstr (P,(Comput (P,s,k))) = halt SCMPDS )
assume LifeSpan (P,s) <= k ; :: thesis: CurInstr (P,(Comput (P,s,k))) = halt SCMPDS
then Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) by A1, EXTPRO_1:6;
hence CurInstr (P,(Comput (P,s,k))) = halt SCMPDS by A1; :: thesis: verum