688      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 

   688      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 

   689      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_read_flag flags))"

   689      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_read_flag flags))"

   690 | "os_grant \<tau> (WriteFile p fd)                = 

   690 | "os_grant \<tau> (WriteFile p fd)                = 

   691     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 

   691     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 

   692      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 

   692      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 

   694 | "os_grant \<tau> (Execve p f fds)                = 

   694 | "os_grant \<tau> (Execve p f fds)                = 

   695     (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> proc_file_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} \<and> fds \<subseteq> current_proc_fds \<tau> p *)

   695     (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> proc_file_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} \<and> fds \<subseteq> current_proc_fds \<tau> p *)

   696 (*

   696 (*

   697 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                = 

   697 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                = 

   698     (p \<in> current_procs \<tau> \<and> f\<^isub>2 \<in> current_files \<tau> \<and> \<not>(f\<^isub>2 \<preceq> f\<^isub>3) \<and> f\<^isub>3 \<notin> current_files \<tau> \<and>

   698     (p \<in> current_procs \<tau> \<and> f\<^isub>2 \<in> current_files \<tau> \<and> \<not>(f\<^isub>2 \<preceq> f\<^isub>3) \<and> f\<^isub>3 \<notin> current_files \<tau> \<and>