for S being COM-Struct
for I being Program of S holds
( card I in dom (stop I) & (stop I) . (card I) = halt S )