let I be Instruction of S; :: thesis: ( I is halting implies I is ins-loc-free )
assume I is halting ; :: thesis: I is ins-loc-free
then A1: JUMP I is empty by Th21;
rng (JumpPart I) c= JUMP I by Def7;
hence JumpPart I is empty by A1, XBOOLE_1:3; :: according to AMISTD_2:def 13 :: thesis: verum