let i be Instruction of SCM+FSA ; :: thesis: for a being Int-Location
for n being Element of NAT st not i destroysdestroy a holds
not IncAddr i,n destroysdestroy a
let a be Int-Location ; :: thesis: for n being Element of NAT st not i destroysdestroy a holds
not IncAddr i,n destroysdestroy a
let n be Element of NAT ; :: thesis: ( not i destroysdestroy a implies not IncAddr i,n destroysdestroy a )
assume A1: not i destroysdestroy a ; :: thesis: not IncAddr i,n destroysdestroy a
A2: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
A3: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A4: 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 A4, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: not IncAddr i,n destroysdestroy a

then i = halt SCM+FSA by SCMFSA_2:122;
then IncAddr i,n = halt SCM+FSA by SCMFSA_4:8;
hence not IncAddr i,n destroysdestroy a by SCMFSA7B:11; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex da, db being Int-Location st i = da := db by SCMFSA_2:54;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:9; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex da, db being Int-Location st i = AddTo da,db by SCMFSA_2:55;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:10; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex da, db being Int-Location st i = SubFrom da,db by SCMFSA_2:56;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:11; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex da, db being Int-Location st i = MultBy da,db by SCMFSA_2:57;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:12; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex da, db being Int-Location st i = Divide da,db by SCMFSA_2:58;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:13; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: not IncAddr i,n destroysdestroy a

then consider loc being Element of NAT such that
A5: i = goto loc by SCMFSA_2:59;
IncAddr i,n = goto (loc + n) by A5, SCMFSA_4:14;
hence not IncAddr i,n destroysdestroy a by SCMFSA7B:17; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: not IncAddr i,n destroysdestroy a

then consider loc being Element of NAT , da being Int-Location such that
A6: i = da =0_goto loc by SCMFSA_2:60;
IncAddr i,n = da =0_goto (loc + n) by A6, SCMFSA_4:15;
hence not IncAddr i,n destroysdestroy a by SCMFSA7B:18; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: not IncAddr i,n destroysdestroy a

then consider loc being Element of NAT , da being Int-Location such that
A7: i = da >0_goto loc by SCMFSA_2:61;
IncAddr i,n = da >0_goto (loc + n) by A7, SCMFSA_4:16;
hence not IncAddr i,n destroysdestroy a by SCMFSA7B:19; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex db, da being Int-Location ex g being FinSeq-Location st i = da := g,db by SCMFSA_2:62;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:17; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex db, da being Int-Location ex g being FinSeq-Location st i = g,db := da by SCMFSA_2:63;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:18; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:64;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:19; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: not IncAddr i,n destroysdestroy a

then ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:65;
hence not IncAddr i,n destroysdestroy a by A1, SCMFSA_4:20; :: thesis: verum

end;

end;