let N be non empty with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st P halts_on s holds
for k being Nat st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; for P being Instruction-Sequence of S
for s being State of S st P halts_on s holds
for k being Nat st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
let P be Instruction-Sequence of S; for s being State of S st P halts_on s holds
for k being Nat st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
let s be State of S; ( P halts_on s implies for k being Nat st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S )
assume
P halts_on s
; for k being 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 Def15;
let k be Nat; ( LifeSpan (P,s) <= k implies CurInstr (P,(Comput (P,s,k))) = halt S )
assume
LifeSpan (P,s) <= k
; CurInstr (P,(Comput (P,s,k))) = halt S
hence
CurInstr (P,(Comput (P,s,k))) = halt S
by A1, Th5; verum