let N be non empty with_non-empty_elements set ; :: thesis: for i being Instruction of (STC N) holds i is jump-only
let i be Instruction of (STC N); :: thesis: i is jump-only
set M = STC N;
let s be State of (STC N); :: according to AMISTD_1:def 3,AMISTD_1:def 4 :: thesis: for o being Object of (STC N)
for I being Instruction of (STC N) st InsCode I = InsCode i & o in Data-Locations (STC N) holds
(Exec (I,s)) . o = s . o
let o be Object of (STC N); :: thesis: for I being Instruction of (STC N) st InsCode I = InsCode i & o in Data-Locations (STC N) holds
(Exec (I,s)) . o = s . o
let I be Instruction of (STC N); :: thesis: ( InsCode I = InsCode i & o in Data-Locations (STC N) implies (Exec (I,s)) . o = s . o )
assume that
InsCode I = InsCode i and
A1: o in Data-Locations (STC N) ; :: thesis: (Exec (I,s)) . o = s . o
A2: the Instruction-Counter of (STC N) = NAT by Def11;
the carrier of (STC N) = NAT \/ {NAT} by Def11;
then Data-Locations (STC N) = (NAT \/ {NAT}) \ ({NAT} \/ NAT) by A2
.= {} by XBOOLE_1:37 ;
hence (Exec (I,s)) . o = s . o by A1; :: thesis: verum