480                                else (sobj = S_proc sp (tagp \<or> tag))

   480                                else (sobj = S_proc sp (tagp \<or> tag))

   481                           else (sobj = S_proc sp tag)

   481                           else (sobj = S_proc sp tag)

   482      | _ \<Rightarrow> sobj = sobj')}"

   482      | _ \<Rightarrow> sobj = sobj')}"

   483 

   483 

   484 

   484 

   486 (* all reachable static states(sobjects set) *)

   486 (* all reachable static states(sobjects set) *)

   487 inductive_set static :: "t_static_state set"

   487 inductive_set static :: "t_static_state set"

   488 where

   488 where

   489   s_init:    "init_static_state \<in> static"

   489   s_init:    "init_static_state \<in> static"

   490 | s_execve:  "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;

   490 | s_execve:  "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;