--- a/Flask.thy	Tue Nov 19 12:31:56 2013 +0800
+++ b/Flask.thy	Wed Nov 20 13:43:09 2013 +0800
@@ -692,7 +692,7 @@
      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 
      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
 | "os_grant \<tau> (Execve p f fds)                = 
-    (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
+    (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 *)
 (*
 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                = 
     (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>
@@ -744,8 +744,8 @@
 | "os_grant \<tau> (ChangeOwner p u)               = (p \<in> current_procs \<tau> \<and> u \<in> current_users \<tau>)"
 *)
 | "os_grant \<tau> (Clone p p' fds shms)           = 
-    (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> current_proc_fds \<tau> p \<and>
-     (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"
+    (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> proc_file_fds \<tau> p \<and>
+     (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))" (* current_proc_fds \<rightarrow> proc_file_fds *)
 | "os_grant \<tau> (Kill p\<^isub>1 p\<^isub>2)                    = 
     (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can kill itself right? *)
 | "os_grant \<tau> (Exit p)                        =