:: deftheorem Def14 defines halt-free COMPOS_1:def 27 :
for S being COM-Struct
for IT being NAT -defined the InstructionsF of b₁ -valued Function holds
( IT is halt-free iff for x being Nat st x in dom IT holds
IT . x <> halt S );