let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Instruction of T st not JUMP i is empty holds
not i is sequential
let T be non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 Nat : verum } ;
assume not JUMP i is empty ; :: thesis: not i is sequential
then consider l being object such that
A1: l in JUMP i ;
reconsider l = l as Nat by A1;
NIC (i,l) in { (NIC (i,l1)) where l1 is Nat : verum } ;
then l in NIC (i,l) by A1, SETFAM_1:def 1;
then consider s being Element of product (the_Values_of T) such that
A2: ( l = IC (Exec (i,s)) & IC s = l ) ;
take s ; :: according to AMISTD_1:def 8 :: thesis: not (Exec (i,s)) . (IC ) = (IC s) + 1
thus not (Exec (i,s)) . (IC ) = (IC s) + 1 by A2; :: thesis: verum