let f be FinSeq-Location ; :: thesis:
let i be Instruction of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
assume A1: not f in UsedInt*Loc i ; :: thesis:
InsCode i <= 12 by SCMFSA_2:16;
then not not InsCode i = 0 & ... & not InsCode i = 12 ;

per cases ;

suppose InsCode i = 0 ; :: thesis:

then i = halt SCM+FSA by SCMFSA_2:95;
hence (Exec (i,s)) . f = s . f by EXTPRO_1:def 3; :: thesis:

end;

suppose InsCode i = 1 ; :: thesis:

then ex a, b being Int-Location st i = a := b by SCMFSA_2:30;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:63; :: thesis:

end;

suppose InsCode i = 2 ; :: thesis:

then ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:31;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:64; :: thesis:

end;

suppose InsCode i = 3 ; :: thesis:

then ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:32;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:65; :: thesis:

end;

suppose InsCode i = 4 ; :: thesis:

then ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:33;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:66; :: thesis:

end;

suppose InsCode i = 5 ; :: thesis:

then ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:34;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:67; :: thesis:

end;

suppose InsCode i = 6 ; :: thesis:

then ex l being Nat st i = goto l by SCMFSA_2:35;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:69; :: thesis:

end;

suppose InsCode i = 7 ; :: thesis:

then ex l being Nat ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:70; :: thesis:

end;

suppose InsCode i = 8 ; :: thesis:

then ex l being Nat ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:71; :: thesis:

end;

suppose InsCode i = 9 ; :: thesis:

then ex a, b being Int-Location ex g being FinSeq-Location st i = b := (g,a) by SCMFSA_2:38;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:72; :: thesis:

end;

suppose InsCode i = 10 ; :: thesis:

then consider a, b being Int-Location, g being FinSeq-Location such that
A2: i = (g,a) := b by SCMFSA_2:39;
UsedInt*Loc i = {g} by A2, Th33;
then f <> g by A1, TARSKI:def 1;
hence (Exec (i,s)) . f = s . f by A2, SCMFSA_2:73; :: thesis:

end;

suppose InsCode i = 11 ; :: thesis:

then ex a being Int-Location ex g being FinSeq-Location st i = a :=len g by SCMFSA_2:40;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:74; :: thesis:

end;

suppose InsCode i = 12 ; :: thesis:

then consider a being Int-Location, g being FinSeq-Location such that
A3: i = g :=<0,...,0> a by SCMFSA_2:41;
UsedInt*Loc i = {g} by A3, Th34;
then f <> g by A1, TARSKI:def 1;
hence (Exec (i,s)) . f = s . f by A3, SCMFSA_2:75; :: thesis:

end;

end;