for f being Instruction-Location of Trivial-AMI IL,N holds NIC I,f = {f} by AMISTD_1:15, AMISTD_1:56;
hence JUMP I is empty by AMISTD_1:14; :: thesis: verum