theory Tainted_prop 
imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
begin

context tainting begin

lemma tainted_in_current:
  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps)




end

end