:: deftheorem defines jump-only AMISTD_1:def 1 :
for N being with_zero set
for S being non empty with_non-empty_values AMI-Struct over N
for T being InsType of the InstructionsF of S holds
( T is jump-only iff for s being State of S
for o being Object of S
for I being Instruction of S st InsCode I = T & o in Data-Locations holds
(Exec (I,s)) . o = s . o );