let N be non empty with_zero set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: 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

hence CurInstr (P,(Comput (P,s,k))) = halt S by A1, Th5; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: 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

hence CurInstr (P,(Comput (P,s,k))) = halt S by A1, Th5; :: thesis: verum