theorem :: COMPOS_1:51

for S being COM-Struct
for I being Program of S
for loc being Nat st loc in dom (stop I) & (stop I) . loc <> halt S holds
loc in dom I