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