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