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

InsCode i <= 12 by SCMFSA_2:16;

then not not InsCode i = 0 & ... & not InsCode i = 12 ;

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

InsCode i <= 12 by SCMFSA_2:16;

then not not InsCode i = 0 & ... & not InsCode i = 12 ;

per cases then
( 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 )
;

end;

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

then
i = halt SCM+FSA
by SCMFSA_2:95;

hence (Exec (i,s)) . f = s . f by EXTPRO_1:def 3; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by EXTPRO_1:def 3; :: thesis: verum

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:30;

hence (Exec (i,s)) . f = s . f by SCMFSA_2:63; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:63; :: thesis: verum

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:31;

hence (Exec (i,s)) . f = s . f by SCMFSA_2:64; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:64; :: thesis: verum

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:32;

hence (Exec (i,s)) . f = s . f by SCMFSA_2:65; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:65; :: thesis: verum

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:33;

hence (Exec (i,s)) . f = s . f by SCMFSA_2:66; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:66; :: thesis: verum

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:34;

hence (Exec (i,s)) . f = s . f by SCMFSA_2:67; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:67; :: thesis: verum

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

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: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:69; :: thesis: verum

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

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: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:70; :: thesis: verum

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

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: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:71; :: thesis: verum

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:38;

hence (Exec (i,s)) . f = s . f by SCMFSA_2:72; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:72; :: thesis: verum

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

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: verum

end;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: verum

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:40;

hence (Exec (i,s)) . f = s . f by SCMFSA_2:74; :: thesis: verum

end;hence (Exec (i,s)) . f = s . f by SCMFSA_2:74; :: thesis: verum

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

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: verum

end;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: verum