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