--- a/Static.thy	Wed Oct 16 14:43:28 2013 +0800
+++ b/Static.thy	Mon Oct 21 16:18:19 2013 +0800
@@ -147,24 +147,23 @@
   "is_many_smsg (Created,sec,tag) = True"
 | "is_many_smsg _                 = False"
 
+(* wrong def 
 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
   "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
 | "is_many_smsgq _                 = False"
+*)
+
+fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
+where
+  "is_many_smsgq (Created,sec,sms) = True"
+| "is_many_smsgq _                 = False"
 
 fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
 where
   "is_many_sshm (Created, sec) = True"
 | "is_many_sshm _              = False"
 
-(*
-fun is_init_sobj :: "t_sobject \<Rightarrow> bool"
-where
-  "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \<noteq> None)"
-| "is_init_sobj (S_file sf tag) = (is_init_sfile sf)"
-| "is_init_sobj (S_dir  sf tag) = (is_init_sfile sf)"
-| "is_init_sobj (S_msg" *)
-
 fun is_many :: "t_sobject \<Rightarrow> bool"
 where
   "is_many (S_proc sp   tag) = is_many_sproc sp"
@@ -173,6 +172,24 @@
 | "is_many (S_msgq sq      ) = is_many_smsgq sq"
 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
 
+fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
+where
+  "is_init_smsgq (Init q,sec,sms) = True"
+| "is_init_smsgq _                = False"
+
+fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
+where
+  "is_init_sshm (Init h,sec) = True"
+| "is_init_sshm _            = False"
+
+fun is_init_sobj :: "t_sobject \<Rightarrow> bool"
+where
+  "is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
+| "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
+| "is_init_sobj (S_dir  sf     ) = is_init_sfile sf"
+| "is_init_sobj (S_msgq sq     ) = is_init_smsgq sq"
+| "is_init_sobj (S_shm  sh     ) = is_init_sshm sh"
+
 (*
 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
 where