theorem :: SCMFSA_2:86

for la being Nat
for a being Int-Location holds not a >0_goto la is halting ;