diff -r d9dc04c3ea90 -r dfde07c7cd6b no_shm_selinux/Static.thy
--- a/no_shm_selinux/Static.thy	Thu Jan 09 14:39:00 2014 +0800
+++ b/no_shm_selinux/Static.thy	Thu Jan 09 19:09:09 2014 +0800
@@ -646,7 +646,6 @@
   "init_obj_related (S_proc (pi, sec, fds) tag) (O_proc p') = (pi = Init p')"
 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
-| "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')"
 (*
 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
 
@@ -658,11 +657,13 @@
 
 (***************** for backward proof when Instancing static objects ******************)
 
+(*
 fun all_procs :: "t_state \<Rightarrow> t_process set"
 where
   "all_procs [] = init_procs"
 | "all_procs (Clone p p' fds # s) = insert p' (all_procs s)"
 | "all_procs (e # s) = all_procs s"
+*)
 
 definition next_nat :: "nat set \<Rightarrow> nat"
 where
@@ -672,9 +673,12 @@
 where 
   "new_proc \<tau> = next_nat (current_procs \<tau>)"
 
+(*
 definition brandnew_proc :: "t_state \<Rightarrow> t_process"
 where
   "brandnew_proc s \<equiv> next_nat (all_procs s)"
+*)
+
 
 definition new_inode_num :: "t_state \<Rightarrow> nat"
 where
@@ -698,9 +702,9 @@
 where
   "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)"
 
-definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
+definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname set"
 where
-  "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}"
+  "all_fname_under_dir d \<tau> fs = {fn. \<exists> f. fn # d = f \<and> f \<in> (current_files \<tau> \<union> fs)}"
 
 fun fname_all_a:: "nat \<Rightarrow> t_fname"
 where
@@ -711,13 +715,17 @@
 where
   "fname_length_set fns = length`fns"
 
-definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname"
+definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname"
 where
-  "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)"
+  "next_fname pf \<tau> fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau> fs))) + 1)"
+
+definition new_childf_general:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_file"
+where
+  "new_childf_general pf \<tau> fs = next_fname pf \<tau> fs # pf"
 
 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
 where
-  "new_childf pf \<tau> = next_fname pf \<tau> # pf"
+  "new_childf pf \<tau> = new_childf_general pf \<tau> {}"
 
 end