let i be Instruction of SCM+FSA; :: thesis: for a being Int-Location
for n being Element of NAT st not i destroys a holds
not IncAddr (i,n) destroys a
let a be Int-Location; :: thesis: for n being Element of NAT st not i destroys a holds
not IncAddr (i,n) destroys a
let n be Element of NAT ; :: thesis: ( not i destroys a implies not IncAddr (i,n) destroys a )
assume A1: not i destroys a ; :: thesis: not IncAddr (i,n) destroys 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: not IncAddr (i,n) destroys a

then i = halt SCM+FSA by SCMFSA_2:95;
then IncAddr (i,n) = halt SCM+FSA by COMPOS_0:4;
hence not IncAddr (i,n) destroys a by SCMFSA7B:5; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: not IncAddr (i,n) destroys a

then ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: not IncAddr (i,n) destroys a

then ex da, db being Int-Location st i = AddTo (da,db) by SCMFSA_2:31;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: not IncAddr (i,n) destroys a

then ex da, db being Int-Location st i = SubFrom (da,db) by SCMFSA_2:32;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: not IncAddr (i,n) destroys a

then ex da, db being Int-Location st i = MultBy (da,db) by SCMFSA_2:33;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: not IncAddr (i,n) destroys a

then ex da, db being Int-Location st i = Divide (da,db) by SCMFSA_2:34;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: not IncAddr (i,n) destroys a

then consider loc being Nat such that
A2: i = goto loc by SCMFSA_2:35;
IncAddr (i,n) = goto (loc + n) by A2, SCMFSA_4:1;
hence not IncAddr (i,n) destroys a by SCMFSA7B:11; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: not IncAddr (i,n) destroys a

then consider loc being Nat, da being Int-Location such that
A3: i = da =0_goto loc by SCMFSA_2:36;
IncAddr (i,n) = da =0_goto (loc + n) by A3, SCMFSA_4:2;
hence not IncAddr (i,n) destroys a by SCMFSA7B:12; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: not IncAddr (i,n) destroys a

then consider loc being Nat, da being Int-Location such that
A4: i = da >0_goto loc by SCMFSA_2:37;
IncAddr (i,n) = da >0_goto (loc + n) by A4, SCMFSA_4:3;
hence not IncAddr (i,n) destroys a by SCMFSA7B:13; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: not IncAddr (i,n) destroys a

then ex db, da being Int-Location ex g being FinSeq-Location st i = da := (g,db) by SCMFSA_2:38;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: not IncAddr (i,n) destroys a

then ex db, da being Int-Location ex g being FinSeq-Location st i = (g,db) := da by SCMFSA_2:39;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: not IncAddr (i,n) destroys a

then ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:40;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: not IncAddr (i,n) destroys a

then ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:41;
hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

end;

end;