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

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 A2, A3, A4, NAT_1:8, NAT_1:33;

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

then i = halt SCM+FSA by SCMFSA_2:122;
hence (Exec i,s) . a = s . a by AMI_1:def 8; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A5: i = da := db by SCMFSA_2:54;
da <> a by A1, A5, Def3;
hence (Exec i,s) . a = s . a by A5, SCMFSA_2:89; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A6: i = AddTo da,db by SCMFSA_2:55;
da <> a by A1, A6, Def3;
hence (Exec i,s) . a = s . a by A6, SCMFSA_2:90; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A7: i = SubFrom da,db by SCMFSA_2:56;
da <> a by A1, A7, Def3;
hence (Exec i,s) . a = s . a by A7, SCMFSA_2:91; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A8: i = MultBy da,db by SCMFSA_2:57;
da <> a by A1, A8, Def3;
hence (Exec i,s) . a = s . a by A8, SCMFSA_2:92; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A9: i = Divide da,db by SCMFSA_2:58;
( da <> a & db <> a ) by A1, A9, Def3;
hence (Exec i,s) . a = s . a by A9, SCMFSA_2:93; :: thesis: verum

end;

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

then consider loc being Instruction-Location of SCM+FSA such that
A10: i = goto loc by SCMFSA_2:59;
thus (Exec i,s) . a = s . a by A10, SCMFSA_2:95; :: thesis: verum

end;

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

then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A11: i = da =0_goto loc by SCMFSA_2:60;
thus (Exec i,s) . a = s . a by A11, SCMFSA_2:96; :: thesis: verum

end;

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

then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A12: i = da >0_goto loc by SCMFSA_2:61;
thus (Exec i,s) . a = s . a by A12, SCMFSA_2:97; :: 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
A13: i = da := g,db by SCMFSA_2:62;
da <> a by A1, A13, Def3;
hence (Exec i,s) . a = s . a by A13, SCMFSA_2:98; :: thesis: verum

end;

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

then consider db, da being Int-Location , g being FinSeq-Location such that
A14: i = g,db := da by SCMFSA_2:63;
thus (Exec i,s) . a = s . a by A14, SCMFSA_2:99; :: 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
A15: i = da :=len g by SCMFSA_2:64;
da <> a by A1, A15, Def3;
hence (Exec i,s) . a = s . a by A15, SCMFSA_2:100; :: thesis: verum

end;

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

then consider da being Int-Location , g being FinSeq-Location such that
A16: i = g :=<0,...,0> da by SCMFSA_2:65;
thus (Exec i,s) . a = s . a by A16, SCMFSA_2:101; :: thesis: verum

end;

end;