let N be with_zero 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 1,AMISTD_1:def 2 :: thesis: for o being Object of (STC N)
for I being Instruction of (STC N) st InsCode I = InsCode i & o in Data-Locations 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 holds
(Exec (I,s)) . o = s . o
let I be Instruction of (STC N); :: thesis: ( InsCode I = InsCode i & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
InsCode I = InsCode i and
A1: o in Data-Locations ; :: thesis: (Exec (I,s)) . o = s . o
A2: IC = 0 by Def7;
Data-Locations = {0} \ {0} by A2, Def7
.= {} by XBOOLE_1:37 ;
hence (Exec (I,s)) . o = s . o by A1; :: thesis: verum