let c be Int-Location; :: thesis: for i being Instruction of SCM+FSA
for s being State of SCM+FSA st not c in UsedIntLoc i holds
(Exec (i,s)) . c = s . c

let i be Instruction of SCM+FSA; :: thesis: for s being State of SCM+FSA st not c in UsedIntLoc i holds
(Exec (i,s)) . c = s . c

let s be State of SCM+FSA; :: thesis: ( not c in UsedIntLoc i implies (Exec (i,s)) . c = s . c )
assume A1: not c in UsedIntLoc i ; :: thesis: (Exec (i,s)) . c = s . c
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 ) ;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s)) . c = s . c
end;
suppose InsCode i = 1 ; :: thesis: (Exec (i,s)) . c = s . c
then consider a, b being Int-Location such that
A2: i = a := b by SCMFSA_2:30;
UsedIntLoc i = {a,b} by ;
then c <> a by ;
hence (Exec (i,s)) . c = s . c by ; :: thesis: verum
end;
suppose InsCode i = 2 ; :: thesis: (Exec (i,s)) . c = s . c
then consider a, b being Int-Location such that
A3: i = AddTo (a,b) by SCMFSA_2:31;
UsedIntLoc i = {a,b} by ;
then c <> a by ;
hence (Exec (i,s)) . c = s . c by ; :: thesis: verum
end;
suppose InsCode i = 3 ; :: thesis: (Exec (i,s)) . c = s . c
then consider a, b being Int-Location such that
A4: i = SubFrom (a,b) by SCMFSA_2:32;
UsedIntLoc i = {a,b} by ;
then c <> a by ;
hence (Exec (i,s)) . c = s . c by ; :: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: (Exec (i,s)) . c = s . c
then consider a, b being Int-Location such that
A5: i = MultBy (a,b) by SCMFSA_2:33;
UsedIntLoc i = {a,b} by ;
then c <> a by ;
hence (Exec (i,s)) . c = s . c by ; :: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: (Exec (i,s)) . c = s . c
then consider a, b being Int-Location such that
A6: i = Divide (a,b) by SCMFSA_2:34;
UsedIntLoc i = {a,b} by ;
then ( c <> a & c <> b ) by ;
hence (Exec (i,s)) . c = s . c by ; :: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s)) . c = s . c
then ex l being Nat st i = goto l by SCMFSA_2:35;
hence (Exec (i,s)) . c = s . c by SCMFSA_2:69; :: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: (Exec (i,s)) . c = s . c
then ex l being Nat ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36;
hence (Exec (i,s)) . c = s . c by SCMFSA_2:70; :: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: (Exec (i,s)) . c = s . c
then ex l being Nat ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37;
hence (Exec (i,s)) . c = s . c by SCMFSA_2:71; :: thesis: verum
end;
suppose InsCode i = 9 ; :: thesis: (Exec (i,s)) . c = s . c
then consider a, b being Int-Location, f being FinSeq-Location such that
A7: i = b := (f,a) by SCMFSA_2:38;
UsedIntLoc i = {a,b} by ;
then c <> b by ;
hence (Exec (i,s)) . c = s . c by ; :: thesis: verum
end;
suppose InsCode i = 10 ; :: thesis: (Exec (i,s)) . c = s . c
then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39;
hence (Exec (i,s)) . c = s . c by SCMFSA_2:73; :: thesis: verum
end;
suppose InsCode i = 11 ; :: thesis: (Exec (i,s)) . c = s . c
then consider a being Int-Location, f being FinSeq-Location such that
A8: i = a :=len f by SCMFSA_2:40;
UsedIntLoc i = {a} by ;
then c <> a by ;
hence (Exec (i,s)) . c = s . c by ; :: thesis: verum
end;
suppose InsCode i = 12 ; :: thesis: (Exec (i,s)) . c = s . c
end;
end;