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 (goto i1,R) & o <> IC (SCM R) holds
(Exec b₅,b₃) . b₄ = b₃ . b₄
let o be Object of (SCM R); :: thesis: for I being Instruction of (SCM R) st InsCode I = InsCode (goto i1,R) & o <> IC (SCM R) holds
(Exec b₄,b₂) . b₃ = b₂ . b₃
let I be Instruction of (SCM R); :: thesis: ( InsCode I = InsCode (goto i1,R) & o <> IC (SCM R) implies (Exec b₃,b₁) . b₂ = b₁ . b₂ )
assume that
A1: InsCode I = InsCode (goto i1,R) and
A2: o <> IC (SCM R) ; :: thesis: (Exec b₃,b₁) . b₂ = b₁ . b₂
InsCode (goto i1,R) = 6 by MCART_1:def 1;
then A3: ex i2 being Element of NAT st I = goto i2,R by A1, Th22;

per cases ( o in NAT or o is Data-Location of R ) by A2, Th5;

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 of R ; :: thesis: (Exec b₃,b₁) . b₂ = b₁ . b₂

hence (Exec I,s) . o = s . o by A3, SCMRING2:17; :: thesis: verum

end;

end;

end;

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