(*<*)
theory S2ss_prop
imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop
begin
(*>*)

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 "