99 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
99 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
100 | _ \<Rightarrow> None)" |
100 | _ \<Rightarrow> None)" |
101 | "init_obj2sobj (O_file f) = |
101 | "init_obj2sobj (O_file f) = |
102 Some (S_file (init_cf2sfiles f) |
102 Some (S_file (init_cf2sfiles f) |
103 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))" |
103 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))" |
104 | "init_obj2sobj (O_dir f) = |
104 | "init_obj2sobj (O_dir f) = |
105 (case (init_cf2sfile f) of |
105 (case (init_cf2sfile f) of |
106 Some sf \<Rightarrow> Some (S_dir sf) |
106 Some sf \<Rightarrow> Some (S_dir sf) |
107 | _ \<Rightarrow> None)" |
107 | _ \<Rightarrow> None)" |
108 | "init_obj2sobj (O_msgq q) = |
108 | "init_obj2sobj (O_msgq q) = |
109 (case (init_cq2smsgq q) of |
109 (case (init_cq2smsgq q) of |
110 Some sq \<Rightarrow> Some (S_msgq sq) |
110 Some sq \<Rightarrow> Some (S_msgq sq) |
111 | _ \<Rightarrow> None)" |
111 | _ \<Rightarrow> None)" |
112 | "init_obj2sobj (O_shm h) = |
112 | "init_obj2sobj (O_shm h) = |