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

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