for l being Instruction-Location of SCM R holds NIC (a := r),l = {(Next l)} by Th58;
hence JUMP (a := r) is empty by Lm6; :: thesis: verum