let T be InsType of the InstructionsF of SCM; :: thesis: ( T = InsCode (SCM-goto i1) implies T is jump-only )
assume A1: T = InsCode (SCM-goto i1) ; :: thesis: T is jump-only
let s be State of SCM; :: according to AMISTD_1:def 1 :: thesis: for b₁ being Element of the U1 of SCM
for b₂ being Element of the InstructionsF of SCM holds
( not InsCode b₂ = T or not b₁ in Data-Locations or (Exec (b₂,s)) . b₁ = s . b₁ )
let o be Object of SCM; :: thesis: for b₁ being Element of the InstructionsF of SCM holds
( not InsCode b₁ = T or not o in Data-Locations or (Exec (b₁,s)) . o = s . o )
let I be Instruction of SCM; :: thesis: ( not InsCode I = T or not o in Data-Locations or (Exec (I,s)) . o = s . o )
assume that
A2: InsCode I = T and
A3: o in Data-Locations ; :: thesis: (Exec (I,s)) . o = s . o
InsCode I = 6 by A2, A1;
then A4: ex i2 being Nat st I = SCM-goto i2 by AMI_5:13;
o is Data-Location by A3, AMI_2:def 16, AMI_3:27;
hence (Exec (I,s)) . o = s . o by A4, AMI_3:7; :: thesis: verum