for a1, a2 being Int-Location
for l1, l2 being Nat st a1 >0_goto l1 = a2 >0_goto l2 holds
( a1 = a2 & l1 = l2 )