--- a/no_shm_selinux/Temp.thy	Thu Jan 09 14:39:00 2014 +0800
+++ b/no_shm_selinux/Temp.thy	Thu Jan 09 19:09:09 2014 +0800
@@ -264,11 +264,18 @@
   "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'"
 
 lemma s2ss_included_sobj:
-  "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
+  "\<lbrakk>dalive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
 by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
 
+fun init_dobj_related :: "t_sobject \<Rightarrow> t_dobject \<Rightarrow> bool"
+where
+  "init_dobj_related (S_proc (pi, sec, fds) tag) (D_proc p') = (pi = Init p')"
+| "init_dobj_related (S_file sfs tag) (D_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
+| "init_dobj_related (S_dir sf) (D_dir f) = (sfile_related sf f)"
+| "init_dobj_related _ _ = False"
+
 lemma init_ss_in_prop:
-  "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk>
+  "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; dalive s obj; init_dobj_related sobj obj\<rbrakk>
    \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss"
 apply (simp add:init_ss_in_def init_ss_eq_def)
 apply (erule bexE, erule conjE)