--- a/Static.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Static.thy	Wed May 15 11:21:39 2013 +0800
@@ -49,9 +49,9 @@
     (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
   | _ \<Rightarrow> None)"
 
-definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set"
+definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set"
 where
-  "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf \<and> is_init_file f}"
+  "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}"
 
 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
 where
@@ -117,7 +117,7 @@
      | _ \<Rightarrow> None)"
 | "init_obj2sobj (O_file f) = 
      (if (f \<in> init_files \<and> is_init_file f) 
-      then Some (S_file (init_cfs2sfiles (init_same_inode_files f)) 
+      then Some (S_file (init_cf2sfiles f) 
                         (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))
       else None)"
 | "init_obj2sobj (O_dir f) = 
@@ -697,12 +697,12 @@
 
 (**************** translation from dynamic to static *******************)
 
-definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_sfile option"
+definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
 where
-  "cf2sfile s f Is_file \<equiv>
+  "cf2sfile s f \<equiv>
      case (parent f) of 
-       None \<Rightarrow> if Is_file then None else Some sroot
-     | Some pf \<Rightarrow> if Is_file 
+       None \<Rightarrow> Some sroot
+     | Some pf \<Rightarrow> if (is_file s f) 
      then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
             (Some sec, Some psec, Some asecs) \<Rightarrow>
  Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
@@ -712,16 +712,16 @@
  Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
           | _ \<Rightarrow> None)"
 
-definition cfs2sfiles :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_sfile set"
+definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
 where
-  "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}"
+  "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
 
 (* 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
   "cfd2sfd s p fd \<equiv> 
     (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
-      (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f True) of 
+      (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of 
                                           Some sf \<Rightarrow> Some (sec, flags, sf)
                                         | _       \<Rightarrow> None)
     | _ \<Rightarrow> None)"
@@ -782,10 +782,10 @@
       | _       \<Rightarrow> None)"
 | "co2sobj s (O_file f) = 
      (if (f \<in> current_files s) then 
-        Some (S_file (cfs2sfiles s (same_inode_files s f)) (O_file f \<in> tainted s))
+        Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))
       else None)"
 | "co2sobj s (O_dir f) = 
-     (case (cf2sfile s f False) of
+     (case (cf2sfile s f) of
         Some sf  \<Rightarrow> Some (S_dir sf)
       | _ \<Rightarrow> None)"
 | "co2sobj s (O_msgq q) =