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 holds
( P halts_on s iff ex k being Nat st 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 holds
( P halts_on s iff ex k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S )
let P be Instruction-Sequence of S; :: thesis: for s being State of S holds
( P halts_on s iff ex k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S )
let s be State of S; :: thesis: ( P halts_on s iff ex k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S )
thus ( P halts_on s implies ex k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S ) ; :: thesis: ( ex k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S implies P halts_on s )
given k being Nat such that A1: CurInstr (P,(Comput (P,s,k))) = halt S ; :: thesis: P halts_on s
take k ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,k)) in dom P & CurInstr (P,(Comput (P,s,k))) = halt S )
IC (Comput (P,s,k)) in NAT ;
hence IC (Comput (P,s,k)) in dom P by PARTFUN1:def 2; :: thesis: CurInstr (P,(Comput (P,s,k))) = halt S
thus CurInstr (P,(Comput (P,s,k))) = halt S by A1; :: thesis: verum