theorem :: AMI_3:21

for loc being Nat holds not SCM-goto loc is halting by Lm9;