let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite realistic standard-ins without_implicit_jumps AMI-Struct of N
for I being Instruction of S st I is halting holds
I is ins-loc-free
let S be non empty stored-program IC-Ins-separated steady-programmed definite realistic standard-ins without_implicit_jumps AMI-Struct of N; :: thesis: for I being Instruction of S st I is halting holds
I is ins-loc-free
let I be Instruction of S; :: thesis: ( I is halting implies I is ins-loc-free )
assume A1: I is halting ; :: thesis: I is ins-loc-free
let x be set ; :: according to AMISTD_2:def 12 :: thesis: ( x in dom (AddressPart I) implies (product" (AddressParts (InsCode I))) . x <> NAT )
assume A2: x in dom (AddressPart I) ; :: thesis: (product" (AddressParts (InsCode I))) . x <> NAT
assume (product" (AddressParts (InsCode I))) . x = NAT ; :: thesis: contradiction
then (AddressPart I) . x in JUMP I by A2, Def7;
hence contradiction by A1, Th21; :: thesis: verum