--- a/Static.thy	Fri May 03 08:20:21 2013 +0100
+++ b/Static.thy	Mon May 06 02:04:27 2013 +0800
@@ -51,7 +51,7 @@
 
 definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set"
 where
-  "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf}"
+  "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf \<and> is_init_file f}"
 
 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
 where
@@ -109,10 +109,6 @@
        (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
      | _ \<Rightarrow> None)"
 
-definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"
-where
-  "init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}"
-
 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
 where
   "init_obj2sobj (O_proc p) = 
@@ -720,10 +716,6 @@
 where
   "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}"
 
-definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
-where
-  "same_inode_files s f \<equiv> {f'. inum_of_file s f = inum_of_file s f'}"
-
 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" 
 where