let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for i being Instruction of T st not JUMP i is empty holds
not i is sequential
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for i being Instruction of T st not JUMP i is empty holds
not i is sequential
let i be Instruction of T; :: thesis: ( not JUMP i is empty implies not i is sequential )
set X = { (NIC i,l1) where l1 is Instruction-Location of T : verum } ;
assume not JUMP i is empty ; :: thesis: not i is sequential
then consider l being set such that
A1: l in JUMP i by XBOOLE_0:def 1;
reconsider l = l as Instruction-Location of T by A1, AMI_1:def 4;
NIC i,l in { (NIC i,l1) where l1 is Instruction-Location of T : verum } ;
then l in NIC i,l by A1, SETFAM_1:def 1;
then consider s being State of T such that
A2: ( l = IC (Following s) & IC s = l & s . l = i ) ;
take s ; :: according to AMISTD_1:def 16 :: thesis: not (Exec i,s) . (IC T) = NextLoc (IC s)
thus not (Exec i,s) . (IC T) = NextLoc (IC s) by A2, Th35; :: thesis: verum