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;

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 )
;

end;

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;then IncAddr (i,n) = halt SCM+FSA by COMPOS_0:4;

hence not IncAddr (i,n) destroys a by SCMFSA7B:5; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;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

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;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

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;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

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum

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;hence not IncAddr (i,n) destroys a by A1, COMPOS_0:4; :: thesis: verum