:: deftheorem defines halts_at COMPOS_1:def 12 :
for S being COM-Struct
for p being NAT -defined the InstructionsF of b₁ -valued Function
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );