--- a/S2ss_prop.thy	Wed Aug 28 08:59:12 2013 +0800
+++ b/S2ss_prop.thy	Thu Aug 29 10:01:24 2013 +0800
@@ -4,4 +4,9 @@
 begin
 (*>*)
 
-context tainting_s begin
\ No newline at end of file
+context tainting_s begin
+
+(* 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