per cases ( InsCode I = 0 or InsCode I = 1 ) by AMISTD_1:22;

suppose InsCode I = 0 ; :: thesis: JUMP I is empty

then for f being Instruction-Location of STC N holds NIC I,f = {f} by AMISTD_1:15, AMISTD_1:20;
hence JUMP I is empty by AMISTD_1:14; :: thesis: verum

end;

suppose InsCode I = 1 ; :: thesis: JUMP I is empty

then for f being Instruction-Location of STC N holds NIC I,f = {(NextLoc f)} by AMISTD_1:39;
hence JUMP I is empty by Th18; :: thesis: verum

end;

end;