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

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

then for f being Nat holds NIC (I,f) = {f} by AMISTD_1:2, AMISTD_1:4;
hence JUMP I is empty by AMISTD_1:1; :: thesis: verum

end;

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

then for f being Element of NAT holds NIC (I,f) = {(f + 1)} by AMISTD_1:10;
hence JUMP I is empty by Th2; :: thesis: verum

end;

end;