set S = SCM R;

now :: thesis: for s being State of (SCM R)
for o being Object of (SCM R)
for I being Instruction of (SCM R) st InsCode I = InsCode (goto (i1,R)) & o in Data-Locations holds
(Exec (I,s)) . o = s . o

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 (goto (i1,R)) & o in Data-Locations 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 (goto (i1,R)) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let I be Instruction of (SCM R); :: thesis: ( InsCode I = InsCode (goto (i1,R)) & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (goto (i1,R)) and
A2: o in Data-Locations ; :: thesis: (Exec (I,s)) . o = s . o
A3: ex i2 being Nat st I = goto (i2,R) by A1, Th17;
o in Data-Locations by A2, SCMRING2:22;
then o is Data-Location of R by SCMRING2:1;
hence (Exec (I,s)) . o = s . o by A3, SCMRING2:15; :: thesis: verum

end;

hence for b₁ being InsType of the InstructionsF of (SCM R) st b₁ = InsCode (goto (i1,R)) holds
b₁ is jump-only ; :: thesis: verum