theorem :: SCMFSA_2:84

for la being Nat holds not goto la is halting ;