theorem :: AMI_3:23

for a being Data-Location
for loc being Nat holds not a >0_goto loc is halting by Lm11;