let N be with_non-empty_elements set ; :: thesis: for IL being non trivial set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins without_implicit_jumps AMI-Struct of IL,N
for I being Instruction of S st I is halting holds
I is ins-loc-free
let IL be non trivial set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins without_implicit_jumps AMI-Struct of IL,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 definite realistic standard-ins without_implicit_jumps AMI-Struct of IL,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 <> IL )
assume A2: x in dom (AddressPart I) ; :: thesis: (product" (AddressParts (InsCode I))) . x <> IL
assume (product" (AddressParts (InsCode I))) . x = IL ; :: thesis: contradiction
then (AddressPart I) . x in JUMP I by A2, Def7;
hence contradiction by A1, Th21; :: thesis: verum