--- a/S2ss_prop.thy	Thu Sep 12 18:23:38 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 12 19:00:26 2013 +0800
@@ -766,7 +766,10 @@
 apply (simp add:co2sobj_writefile_unchange alive_simps)
 done
 
-
+lemma s2ss_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
+     case (file_of_proc_fd s p fd) of
+       Some f \<Rightarrow> if ("
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
   s2ss_readfile s2ss_writefile