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

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

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