292      | _      \<Rightarrow> (inum_of_file \<tau>)    )"

   292      | _      \<Rightarrow> (inum_of_file \<tau>)    )"

   293 | "inum_of_file (UnLink p f # \<tau>) = (

   293 | "inum_of_file (UnLink p f # \<tau>) = (

   294      if (proc_fd_of_file \<tau> f = {}) 

   294      if (proc_fd_of_file \<tau> f = {}) 

   295      then (inum_of_file \<tau>) (f := None)

   295      then (inum_of_file \<tau>) (f := None)

   296      else inum_of_file \<tau>            )" 

   296      else inum_of_file \<tau>            )" 

   301 | "inum_of_file (Mkdir p f ino # \<tau>) = (inum_of_file \<tau>) (f:=  Some ino)"

   298 | "inum_of_file (Mkdir p f ino # \<tau>) = (inum_of_file \<tau>) (f:=  Some ino)"

   302 | "inum_of_file (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = (inum_of_file \<tau>) (f\<^isub>2 := inum_of_file \<tau> f\<^isub>1)"

   299 | "inum_of_file (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = (inum_of_file \<tau>) (f\<^isub>2 := inum_of_file \<tau> f\<^isub>1)"

   303 (*

   300 (*

   304 | "inum_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = (\<lambda> f. 

   301 | "inum_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = (\<lambda> f. 

   305      if (f\<^isub>2 \<preceq> f) then None

   302      if (f\<^isub>2 \<preceq> f) then None

   742                                        (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   739                                        (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   743                                        (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   740                                        (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   744                                        deleted obj s)"

   741                                        deleted obj s)"

   745 | "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or> 

   742 | "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or> 

   746                                             deleted obj s)"

   743                                             deleted obj s)"

   748 | "deleted obj (Rmdir p f # s)  = ((obj = O_dir  f) \<or> deleted obj s)"

   745 | "deleted obj (Rmdir p f # s)  = ((obj = O_dir  f) \<or> deleted obj s)"

   749 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> 

   746 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> 

   750                                (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or>

   747                                (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or>

   751                                (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> deleted obj s)"

   748                                (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> deleted obj s)"

   752 (*

   749 (*