let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for I being Instruction of S st ( for f being Instruction-Location of S holds NIC I,f = {(NextLoc f)} ) holds
JUMP I is empty
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for I being Instruction of S st ( for f being Instruction-Location of S holds NIC I,f = {(NextLoc f)} ) holds
JUMP I is empty
let I be Instruction of S; :: thesis: ( ( for f being Instruction-Location of S holds NIC I,f = {(NextLoc f)} ) implies JUMP I is empty )
assume A1: for f being Instruction-Location of S holds NIC I,f = {(NextLoc f)} ; :: thesis: JUMP I is empty
set p = 1;
set q = 2;
reconsider p = 1, q = 2 as Instruction-Location of S by AMI_1:def 4;
set X = { (NIC I,f) where f is Instruction-Location of S : verum } ;
assume not JUMP I is empty ; :: thesis: contradiction
then consider x being set such that
A3: x in meet { (NIC I,f) where f is Instruction-Location of S : verum } by XBOOLE_0:def 1;
( NIC I,p = {(NextLoc p)} & NIC I,q = {(NextLoc q)} ) by A1;
then ( {(NextLoc p)} in { (NIC I,f) where f is Instruction-Location of S : verum } & {(NextLoc q)} in { (NIC I,f) where f is Instruction-Location of S : verum } ) ;
then ( x in {(NextLoc p)} & x in {(NextLoc q)} ) by A3, SETFAM_1:def 1;
then ( x = NextLoc p & x = NextLoc q ) by TARSKI:def 1;
hence contradiction by AMISTD_1:36; :: thesis: verum