let N be 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 NAT ,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 NAT ,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) & (product" (AddressParts (InsCode I))) . k = NAT ) by Def12;
(AddressPart I) . k in JUMP I by A2, Def7;
hence contradiction by A1, AMISTD_1:43; :: thesis: verum