:: deftheorem Def3 defines halting EXTPRO_1:def 3 :
for N being with_zero set
for S being with_non-empty_values AMI-Struct over N
for I being Instruction of S holds
( I is halting iff for s being State of S holds Exec (I,s) = s );