let aa be Int-Location ; :: thesis: for I being Program of SCM+FSA st not aa in UsedIntLoc I holds
I does_not_destroy aa
let I be Program of SCM+FSA ; :: thesis: ( not aa in UsedIntLoc I implies I does_not_destroy aa )
assume A1: not aa in UsedIntLoc I ; :: thesis: I does_not_destroy aa
let i be Instruction of SCM+FSA ; :: according to SCMFSA7B:def 4 :: thesis: ( not i in proj2 I or i does_not_destroy aa )
assume i in rng I ; :: thesis: i does_not_destroy aa
then UsedIntLoc i c= UsedIntLoc I by SF_MASTR:23;
then A2: not aa in UsedIntLoc i by A1;
A3: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
A4: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A5: 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 A5, A4, A3, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: i does_not_destroy aa

then i = halt SCM+FSA by SCMFSA_2:122;
hence i does_not_destroy aa by SCMFSA7B:11; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: i does_not_destroy aa

then consider a, b being Int-Location such that
A6: i = a := b by SCMFSA_2:54;
UsedIntLoc i = {a,b} by A6, SF_MASTR:18;
then a in UsedIntLoc i by TARSKI:def 2;
hence i does_not_destroy aa by A2, A6, SCMFSA7B:12; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: i does_not_destroy aa

then consider a, b being Int-Location such that
A7: i = AddTo a,b by SCMFSA_2:55;
UsedIntLoc i = {a,b} by A7, SF_MASTR:18;
then a in UsedIntLoc i by TARSKI:def 2;
hence i does_not_destroy aa by A2, A7, SCMFSA7B:13; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: i does_not_destroy aa

then consider a, b being Int-Location such that
A8: i = SubFrom a,b by SCMFSA_2:56;
UsedIntLoc i = {a,b} by A8, SF_MASTR:18;
then a in UsedIntLoc i by TARSKI:def 2;
hence i does_not_destroy aa by A2, A8, SCMFSA7B:14; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: i does_not_destroy aa

then consider a, b being Int-Location such that
A9: i = MultBy a,b by SCMFSA_2:57;
UsedIntLoc i = {a,b} by A9, SF_MASTR:18;
then a in UsedIntLoc i by TARSKI:def 2;
hence i does_not_destroy aa by A2, A9, SCMFSA7B:15; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: i does_not_destroy aa

then consider a, b being Int-Location such that
A10: i = Divide a,b by SCMFSA_2:58;
A11: UsedIntLoc i = {a,b} by A10, SF_MASTR:18;
then A12: b in UsedIntLoc i by TARSKI:def 2;
a in UsedIntLoc i by A11, TARSKI:def 2;
hence i does_not_destroy aa by A2, A10, A12, SCMFSA7B:16; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: i does_not_destroy aa

then ex l being Element of NAT st i = goto l by SCMFSA_2:59;
hence i does_not_destroy aa by SCMFSA7B:17; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: i does_not_destroy aa

then ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:60;
hence i does_not_destroy aa by SCMFSA7B:18; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: i does_not_destroy aa

then ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:61;
hence i does_not_destroy aa by SCMFSA7B:19; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: i does_not_destroy aa

then consider a, b being Int-Location , f being FinSeq-Location such that
A13: i = b := f,a by SCMFSA_2:62;
UsedIntLoc i = {a,b} by A13, SF_MASTR:21;
then b in UsedIntLoc i by TARSKI:def 2;
hence i does_not_destroy aa by A2, A13, SCMFSA7B:20; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: i does_not_destroy aa

then ex a, b being Int-Location ex f being FinSeq-Location st i = f,a := b by SCMFSA_2:63;
hence i does_not_destroy aa by SCMFSA7B:21; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: i does_not_destroy aa

then consider a being Int-Location , f being FinSeq-Location such that
A14: i = a :=len f by SCMFSA_2:64;
UsedIntLoc i = {a} by A14, SF_MASTR:22;
then a in UsedIntLoc i by TARSKI:def 1;
hence i does_not_destroy aa by A2, A14, SCMFSA7B:22; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: i does_not_destroy aa

then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:65;
hence i does_not_destroy aa by SCMFSA7B:23; :: thesis: verum

end;

end;