set S = SCM R;

now

let s be State of (SCM R); :: thesis: for o being Object of (SCM R)
for I being Instruction of (SCM R) st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations (SCM R) holds
(Exec (I,s)) . o = s . o
let o be Object of (SCM R); :: thesis: for I being Instruction of (SCM R) st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations (SCM R) holds
(Exec (I,s)) . o = s . o
let I be Instruction of (SCM R); :: thesis: ( InsCode I = InsCode (a =0_goto i1) & o in Data-Locations (SCM R) implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (a =0_goto i1) and
A2: o in Data-Locations (SCM R) ; :: thesis: (Exec (I,s)) . o = s . o
InsCode (a =0_goto i1) = 7 by RECDEF_2:def 1;
then A3: ex b being Data-Location of R ex i2 being Element of NAT st I = b =0_goto i2 by A1, Th23;
o in Data-Locations SCM by A2, SCMRING2:31;
then o is Data-Location of R by SCMRING2:1;
hence (Exec (I,s)) . o = s . o by A3, SCMRING2:18; :: thesis: verum

end;

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