let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of 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 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 Element of NAT : 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 Element of NAT by A1;
NIC i,l in { (NIC i,l1) where l1 is Element of NAT : verum } ;
then l in NIC i,l by A1, SETFAM_1:def 1;
then consider s being Element of product the Object-Kind of T such that
A2: ( l = IC (Following (ProgramPart s),s) & IC s = l & (ProgramPart s) /. l = i ) ;
take s ; :: according to AMISTD_1:def 16 :: thesis: not (Exec i,s) . (IC T) = NextLoc (IC s),T
thus not (Exec i,s) . (IC T) = NextLoc (IC s),T by A2, Th35; :: thesis: verum