:: deftheorem defines >0_goto AMI_3:def 10 :
for loc being Nat
for a being Data-Location holds a >0_goto loc = [8,<*loc*>,<*a*>];