(*<*)
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) = (
     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> {} "