let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA 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 SCM+FSA
let s be State of SCM+FSA; :: 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 SCM+FSA )
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 SCM+FSA
then A1: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt SCM+FSA by EXTPRO_1:def 14;
let k be Element of NAT ; :: thesis: ( LifeSpan (P,s) <= k implies CurInstr (P,(Comput (P,s,k))) = halt SCM+FSA )
set i = LifeSpan (P,s);
assume LifeSpan (P,s) <= k ; :: thesis: CurInstr (P,(Comput (P,s,k))) = halt SCM+FSA
hence CurInstr (P,(Comput (P,s,k))) = halt SCM+FSA by A1, EXTPRO_1:6; :: thesis: verum