let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated halting AMI-Struct of N
for P being Instruction-Sequence of S
for s being State of S 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 S
let S be non empty IC-Ins-separated halting AMI-Struct of N; :: thesis: for P being Instruction-Sequence of S
for s being State of S 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 S
let P be Instruction-Sequence of S; :: thesis: for s being State of S 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 S
let s be State of S; :: 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 S )
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 S
then A1: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by Def14;
let k be Element of NAT ; :: thesis: ( LifeSpan (P,s) <= k implies CurInstr (P,(Comput (P,s,k))) = halt S )
assume LifeSpan (P,s) <= k ; :: thesis: CurInstr (P,(Comput (P,s,k))) = halt S
then Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) by A1, Th6;
hence CurInstr (P,(Comput (P,s,k))) = halt S by A1; :: thesis: verum