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