theorem :: EXTPRO_1:29

for N being 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 holds
( P halts_on s iff ex k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S )