let N be with_non-empty_elements set ; :: thesis: for IL being non trivial set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins with_explicit_jumps AMI-Struct of IL,N
for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
let IL be non trivial set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins with_explicit_jumps AMI-Struct of IL,N
for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
let S be non empty stored-program halting IC-Ins-separated definite realistic standard-ins with_explicit_jumps AMI-Struct of IL,N; :: thesis: for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
let I be Instruction of S; :: thesis: ( I is ins-loc-free implies JUMP I is empty )
assume A1: for x being set st x in dom (AddressPart I) holds
(product" (AddressParts (InsCode I))) . x <> IL ; :: according to AMISTD_2:def 12 :: thesis: JUMP I is empty
assume not JUMP I is empty ; :: thesis: contradiction
then consider f being set such that
A2: f in JUMP I by XBOOLE_0:def 1;
ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL ) by A2, Def6;
hence contradiction by A1; :: thesis: verum