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