equal
deleted
inserted
replaced
216 not_deleted_cur_udp_app not_deleted_cur_shm_app not_deleted_cur_msgq_app |
216 not_deleted_cur_udp_app not_deleted_cur_shm_app not_deleted_cur_msgq_app |
217 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
217 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
218 current_msg_imp_current_msgq) |
218 current_msg_imp_current_msgq) |
219 done |
219 done |
220 |
220 |
|
221 lemma not_deleted_imp_alive_cons: |
|
222 "\<lbrakk>\<not> deleted obj (e # s); valid (e # s); alive s obj\<rbrakk> \<Longrightarrow> alive (e # s) obj" |
|
223 using not_deleted_imp_alive_app[where s = s and s' = "[e]" and obj = obj] |
|
224 by auto |
|
225 |
221 (* |
226 (* |
222 |
227 |
223 lemma nodel_imp_un_deleted: |
228 lemma nodel_imp_un_deleted: |
224 "no_del_event s \<Longrightarrow> \<not> deleted obj s" |
229 "no_del_event s \<Longrightarrow> \<not> deleted obj s" |
225 by (induct s, simp, case_tac a,auto) |
230 by (induct s, simp, case_tac a,auto) |