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 F being Instruction-Sequence of S
for s being State of S st ex k being Nat st F . (IC (Comput (F,s,k))) = halt S holds
F halts_on s