diff -r 6884b3c9284b -r e7f850d1e08e S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/S2ss_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -9,4 +9,6 @@
 (* simpset for s2ss*)
 
 lemma s2ss_execve:
-  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = s2ss s "
\ No newline at end of file
+  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
+     if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
+     then (case (cp2sproc (Execve p f fds # s)  s2ss s \<union> {} "
\ No newline at end of file