theorem :: SCMFSA_2:85

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