let aa be Int-Location; :: thesis: for I being Program of SCM+FSA st not aa in UsedILoc I holds
not I destroys aa
let I be Program of SCM+FSA; :: thesis: ( not aa in UsedILoc I implies not I destroys aa )
assume A1: not aa in UsedILoc I ; :: thesis: not I destroys aa
let i be Instruction of SCM+FSA; :: according to SCMFSA7B:def 4 :: thesis: ( not i in rng I or not i destroys aa )
assume i in rng I ; :: thesis: not i destroys aa
then UsedIntLoc i c= UsedILoc I by SF_MASTR:19;
then A2: not aa in UsedIntLoc i by A1;
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: not i destroys aa

then i = halt SCM+FSA by SCMFSA_2:95;
hence not i destroys aa ; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: not i destroys aa

then consider a, b being Int-Location such that
A3: i = a := b by SCMFSA_2:30;
UsedIntLoc i = {a,b} by A3, SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence not i destroys aa by A2, A3, SCMFSA7B:6; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: not i destroys aa

then consider a, b being Int-Location such that
A4: i = AddTo (a,b) by SCMFSA_2:31;
UsedIntLoc i = {a,b} by A4, SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence not i destroys aa by A2, A4, SCMFSA7B:7; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: not i destroys aa

then consider a, b being Int-Location such that
A5: i = SubFrom (a,b) by SCMFSA_2:32;
UsedIntLoc i = {a,b} by A5, SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence not i destroys aa by A2, A5, SCMFSA7B:8; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: not i destroys aa

then consider a, b being Int-Location such that
A6: i = MultBy (a,b) by SCMFSA_2:33;
UsedIntLoc i = {a,b} by A6, SF_MASTR:14;
then a in UsedIntLoc i by TARSKI:def 2;
hence not i destroys aa by A2, A6, SCMFSA7B:9; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: not i destroys aa

then consider a, b being Int-Location such that
A7: i = Divide (a,b) by SCMFSA_2:34;
A8: UsedIntLoc i = {a,b} by A7, SF_MASTR:14;
then A9: b in UsedIntLoc i by TARSKI:def 2;
a in UsedIntLoc i by A8, TARSKI:def 2;
hence not i destroys aa by A2, A7, A9, SCMFSA7B:10; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: not i destroys aa

then ex l being Nat st i = goto l by SCMFSA_2:35;
hence not i destroys aa ; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: not i destroys aa

then ex l being Nat ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36;
hence not i destroys aa ; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: not i destroys aa

then ex l being Nat ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37;
hence not i destroys aa ; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: not i destroys aa

then consider a, b being Int-Location, f being FinSeq-Location such that
A10: i = b := (f,a) by SCMFSA_2:38;
UsedIntLoc i = {a,b} by A10, SF_MASTR:17;
then b in UsedIntLoc i by TARSKI:def 2;
hence not i destroys aa by A2, A10, SCMFSA7B:14; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: not i destroys aa

then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39;
hence not i destroys aa by SCMFSA7B:15; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: not i destroys aa

then consider a being Int-Location, f being FinSeq-Location such that
A11: i = a :=len f by SCMFSA_2:40;
UsedIntLoc i = {a} by A11, SF_MASTR:18;
then a in UsedIntLoc i by TARSKI:def 1;
hence not i destroys aa by A2, A11, SCMFSA7B:16; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: not i destroys aa

then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41;
hence not i destroys aa by SCMFSA7B:17; :: thesis: verum

end;

end;