let f be FinSeq-Location ; :: thesis: for i being Instruction of SCM+FSA
for s being State of SCM+FSA st not f in UsedInt*Loc i holds
(Exec (i,s)) . f = s . f
let i be Instruction of SCM+FSA; :: thesis: for s being State of SCM+FSA st not f in UsedInt*Loc i holds
(Exec (i,s)) . f = s . f
let s be State of SCM+FSA; :: thesis: ( not f in UsedInt*Loc i implies (Exec (i,s)) . f = s . f )
assume A1: not f in UsedInt*Loc i ; :: thesis: (Exec (i,s)) . f = s . f
A2: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
A3: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A4: InsCode i <= 11 + 1 by SCMFSA_2:35;

per cases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A4, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 1 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 2 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 3 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 4 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 5 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 6 ; :: thesis: (Exec (i,s)) . f = s . f

then ex l being Element of NAT st i = goto l by SCMFSA_2:59;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:95; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (Exec (i,s)) . f = s . f

then ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:60;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:96; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (Exec (i,s)) . f = s . f

then ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:61;
hence (Exec (i,s)) . f = s . f by SCMFSA_2:97; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 10 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 11 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

suppose InsCode i = 12 ; :: thesis: (Exec (i,s)) . f = s . f

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

end;

end;