theorem :: AMI_3:22
for a being Data-Location
for loc being Nat holds not a =0_goto loc is halting by Lm10;