let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps AMI-Struct of N
for I being Instruction of S st I is sequential holds
I is ins-loc-free
let S be non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps AMI-Struct of N; :: thesis: for I being Instruction of S st I is sequential holds
I is ins-loc-free
let I be Instruction of S; :: thesis: ( I is sequential implies I is ins-loc-free )
assume A1: I is sequential ; :: thesis: I is ins-loc-free
assume not I is ins-loc-free ; :: thesis: contradiction
then consider k being set such that
A2: k in dom (AddressPart I) and
A3: (product" (AddressParts (InsCode I))) . k = NAT by Def12;
(AddressPart I) . k in JUMP I by A2, A3, Def7;
hence contradiction by A1, AMISTD_1:43; :: thesis: verum