for l being Element of NAT holds NIC ((a := r),l) = {(l + 1)} by AMISTD_1:12;
hence JUMP (a := r) is empty by Lm3; :: thesis: verum