155   and init_procfds_valid:      "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)"

   155   and init_procfds_valid:      "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)"

   156   and init_filefd_valid:       "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)"

   156   and init_filefd_valid:       "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)"

   157   and init_fileflag_valid:     "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"

   157   and init_fileflag_valid:     "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"

   158 

   158 

   159   and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"

   159   and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"

   160   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"

   161   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"

   161   and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"

   162   and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"

   162 

   163 

   163   and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p"

   164   and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p"

   164   and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"

   165   and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"

   424   "current_shms [] = init_shms"

   425   "current_shms [] = init_shms"

   425 | "current_shms (CreateShM p newshm # \<tau>) = insert newshm (current_shms \<tau>)"

   426 | "current_shms (CreateShM p newshm # \<tau>) = insert newshm (current_shms \<tau>)"

   426 | "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"

   427 | "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"

   427 | "current_shms (e # \<tau>) = current_shms \<tau> "

   428 | "current_shms (e # \<tau>) = current_shms \<tau> "

   428 

   429 

   430 where

   431 where

   431   "procs_of_shm [] = init_procs_of_shm"

   432   "procs_of_shm [] = init_procs_of_shm"

   432 | "procs_of_shm (CreateShM p h # \<tau>) = 

   433 | "procs_of_shm (CreateShM p h # \<tau>) = 

   433     (procs_of_shm \<tau>) (h := {})"  (* creator may not be the sharer of the shm *)

   434     (procs_of_shm \<tau>) (h := {})"  (* creator may not be the sharer of the shm *)

   434 | "procs_of_shm (Attach p h flag # \<tau>) = 

   435 | "procs_of_shm (Attach p h flag # \<tau>) =