227 

   227 

   228 lemma nodel_imp_un_deleted:

   228 lemma nodel_imp_un_deleted:

   229   "no_del_event s \<Longrightarrow> \<not> deleted obj s"

   229   "no_del_event s \<Longrightarrow> \<not> deleted obj s"

   230 by (induct s, simp, case_tac a,auto)

   230 by (induct s, simp, case_tac a,auto)

   231 

   231 

   232 lemma nodel_exists_remains:

   233 lemma nodel_exists_remains:

   233   "\<lbrakk>no_del_event (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"

   234   "\<lbrakk>no_del_event (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"

   234 apply (drule_tac obj = obj in nodel_imp_un_deleted)

   235 apply (drule_tac obj = obj in nodel_imp_un_deleted)

   235 by (simp add:not_deleted_imp_exists')

   236 by (simp add:not_deleted_imp_exists')

   236 

   237