12 

    12 

    13 definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

    13 definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

    14 where

    14 where

    15   "add_ss ss so \<equiv> ss \<union> {so}"

    15   "add_ss ss so \<equiv> ss \<union> {so}"

    16 

    16 

    17 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

    18 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

    18 where

    19 where

    19   "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"

    20   "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"

    20 

    23 

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

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

    22 inductive_set static :: "t_static_state set"

    25 inductive_set static :: "t_static_state set"

    23 where

    26 where

    24   s_init:    "init_static_state \<in> static"

    27   s_init:    "init_static_state \<in> static"