set S = SCM ;

now

let s be State of SCM; :: thesis: for o being Object of SCM
for I being Instruction of SCM st InsCode I = InsCode (SCM-goto i1) & o in Data-Locations SCM holds
(Exec (I,s)) . o = s . o
let o be Object of SCM; :: thesis: for I being Instruction of SCM st InsCode I = InsCode (SCM-goto i1) & o in Data-Locations SCM holds
(Exec (I,s)) . o = s . o
let I be Instruction of SCM; :: thesis: ( InsCode I = InsCode (SCM-goto i1) & o in Data-Locations SCM implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (SCM-goto i1) and
A2: o in Data-Locations SCM ; :: thesis: (Exec (I,s)) . o = s . o
InsCode I = 6 by A1, RECDEF_2:def 1;
then A3: ex i2 being Element of NAT st I = SCM-goto i2 by AMI_5:52;
o is Data-Location by A2, AMI_3:72, AMI_3:def 2;
hence (Exec (I,s)) . o = s . o by A3, AMI_3:13; :: thesis: verum

end;

hence for b₁ being InsType of SCM st b₁ = InsCode (SCM-goto i1) holds
b₁ is jump-only by AMISTD_1:def 3; :: thesis: verum