let N be with_non-empty_elements set ; :: thesis: for i being Instruction of holds i is jump-only
let i be Instruction of ; :: thesis: i is jump-only
set M = STC N;
let s be State of ; :: according to AMISTD_1:def 3,AMISTD_1:def 4 :: thesis: for o being Object of
for I being Instruction of st InsCode I = InsCode i & o <> IC (STC N) holds
(Exec I,s) . o = s . o
let o be Object of ; :: thesis: for I being Instruction of st InsCode I = InsCode i & o <> IC (STC N) holds
(Exec I,s) . o = s . o
let I be Instruction of ; :: thesis: ( InsCode I = InsCode i & o <> IC (STC N) implies (Exec I,s) . o = s . o )
assume that
InsCode I = InsCode i and
A1: o <> IC (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 ( o in NAT or o in {NAT } ) by XBOOLE_0:def 3;
then reconsider l = o as Instruction-Location of STC N by A2, A1, AMI_1:def 4, TARSKI:def 1;
(Exec i,s) . l = s . l by AMI_1:def 13;
hence (Exec I,s) . o = s . o by AMI_1:def 13; :: thesis: verum