for l being Element of NAT holds NIC ((a := r),l) = {(succ l)} by Th58;
hence JUMP (a := r) is empty by Lm5; :: thesis: verum