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 (Exec (i,s)) & IC s = l ) ;
take s ; :: according to AMISTD_1:def 16 :: thesis: not (Exec (i,s)) . (IC T) = succ (IC s)
thus not (Exec (i,s)) . (IC T) = succ (IC s) by A2; :: thesis: verum