set S = SCM ;

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

let s be State of SCM; :: thesis: for o being Object of SCM
for I being Instruction of SCM st InsCode I = InsCode (a >0_goto i1) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let o be Object of SCM; :: thesis: for I being Instruction of SCM st InsCode I = InsCode (a >0_goto i1) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let I be Instruction of SCM; :: thesis: ( InsCode I = InsCode (a >0_goto i1) & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
A4: InsCode I = InsCode (a >0_goto i1) and
A5: o in Data-Locations ; :: thesis: (Exec (I,s)) . o = s . o
InsCode I = 8 by A4;
then A6: ex i2 being Nat ex b being Data-Location st I = b >0_goto i2 by AMI_5:15;
o is Data-Location by A5, AMI_2:def 16, AMI_3:27;
hence (Exec (I,s)) . o = s . o by A6, AMI_3:9; :: thesis: verum

end;

hence for b₁ being InsType of the InstructionsF of SCM st b₁ = InsCode (a >0_goto i1) holds
b₁ is jump-only ; :: thesis: verum