--- a/no_shm_selinux/Init_prop.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Init_prop.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -791,7 +791,7 @@
 *)
 
 lemma co2sobj_nil_prop:
-  "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
+  "init_dalive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
 apply (case_tac obj)
 apply (auto simp add:cf2sfile_nil_prop (*cq2smsga_nil_prop cqm2sms_nil_prop*) tainted_nil_prop 
                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1
@@ -802,9 +802,15 @@
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
 done
 
+lemma init_dalive_prop: "init_dalive obj = dalive [] obj"
+apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props
+         is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil
+         is_tcp_sock_nil is_udp_sock_nil)
+done
+
 lemma s2ss_nil_prop:
   "s2ss [] = init_static_state"
-using co2sobj_nil_prop init_alive_prop
+using co2sobj_nil_prop init_dalive_prop
 by (auto simp add:s2ss_def init_static_state_def)
 
 end