set S = SCM+FSA ;

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

let s be State of SCM+FSA; :: thesis: for o being Object of SCM+FSA
for I being Instruction of SCM+FSA st InsCode I = InsCode (goto i1) & o in Data-Locations holds
(Exec (b₅,b₃)) . b₄ = b₃ . b₄
let o be Object of SCM+FSA; :: thesis: for I being Instruction of SCM+FSA st InsCode I = InsCode (goto i1) & o in Data-Locations holds
(Exec (b₄,b₂)) . b₃ = b₂ . b₃
let I be Instruction of SCM+FSA; :: thesis: ( InsCode I = InsCode (goto i1) & o in Data-Locations implies (Exec (b₃,b₁)) . b₂ = b₁ . b₂ )
assume that
A1: InsCode I = InsCode (goto i1) and
A2: o in Data-Locations ; :: thesis: (Exec (b₃,b₁)) . b₂ = b₁ . b₂
A3: ex i2 being Nat st I = goto i2 by A1, SCMFSA_2:35;

per cases ( o is Int-Location or o is FinSeq-Location ) by A2, Th1;

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

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

end;

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

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

end;

end;

end;

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