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 (a >0_goto i1) & o <> IC SCM holds
(Exec b₅,b₃) . b₄ = b₃ . b₄
let o be Object of SCM ; :: thesis: for I being Instruction of SCM st InsCode I = InsCode (a >0_goto i1) & o <> IC SCM holds
(Exec b₄,b₂) . b₃ = b₂ . b₃
let I be Instruction of SCM ; :: thesis: ( InsCode I = InsCode (a >0_goto i1) & o <> IC SCM implies (Exec b₃,b₁) . b₂ = b₁ . b₂ )
assume that
A4: InsCode I = InsCode (a >0_goto i1) and
A5: o <> IC SCM ; :: thesis: (Exec b₃,b₁) . b₂ = b₁ . b₂
InsCode I = 8 by A4, RECDEF_2:def 1;
then A6: ex i2 being Element of NAT ex b being Data-Location st I = b >0_goto i2 by AMI_5:54;

per cases ( o in NAT or o is Data-Location ) by A5, Th3;

suppose o in NAT ; :: thesis: (Exec b₃,b₁) . b₂ = b₁ . b₂

then reconsider l = o as Element of NAT ;
l = o ;
hence (Exec I,s) . o = s . o by AMI_1:def 13; :: thesis: verum

end;

suppose o is Data-Location ; :: thesis: (Exec b₃,b₁) . b₂ = b₁ . b₂

hence (Exec I,s) . o = s . o by A6, AMI_3:15; :: thesis: verum

end;

end;

end;

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