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

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