diff -r b992684e9ff6 -r dcde836219bc all_sobj_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/all_sobj_prop.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,2246 @@
+theory all_sobj_prop
+imports Main rc_theory os_rc obj2sobj_prop deleted_prop sound_defs_prop source_prop
+begin
+
+context tainting_s_complete begin
+
+lemma initf_has_effinitialrole:
+  "f \<in> init_files ==> \<exists> r. effinitialrole [] f = Some r"
+by (rule_tac f = f in file_has_effinitialrole, simp, simp add:vs_nil)
+
+lemma initf_has_effforcedrole:
+  "f \<in> init_files ==> \<exists> r. effforcedrole [] f = Some r"
+by (rule_tac f = f in file_has_effforcedrole, simp, simp add:vs_nil)
+
+lemma efffrole_sdir_some:
+  "sd \<in> init_files ==> \<exists> r. erole_functor init_file_forcedrole InheritUpMixed sd = Some r"
+apply (frule_tac s = "[]" in undel_initf_keeps_efrole, simp, simp add:vs_nil)
+by (drule initf_has_effforcedrole, simp)
+
+lemma efffrole_sdir_some':
+  "erole_functor init_file_forcedrole InheritUpMixed sd = None ==> sd \<notin> init_files"
+by (rule notI, auto dest!:efffrole_sdir_some)
+
+lemma effirole_sdir_some:
+  "sd \<in> init_files ==> \<exists> r. erole_functor init_file_initialrole UseForcedRole sd = Some r"
+apply (frule_tac s = "[]" in undel_initf_keeps_eirole, simp, simp add:vs_nil)
+by (drule initf_has_effinitialrole, simp)
+
+lemma effirole_sdir_some':
+  "erole_functor init_file_initialrole UseForcedRole sd = None ==> sd \<notin> init_files"
+by (rule notI, auto dest:effirole_sdir_some)
+
+lemma erole_func_irole_simp:
+  "erole_functor init_file_initialrole UseForcedRole sd = effinitialrole [] sd"
+by (simp add:effinitialrole_def)
+
+lemma erole_func_frole_simp:
+  "erole_functor init_file_forcedrole InheritUpMixed sd = effforcedrole [] sd"
+by (simp add:effforcedrole_def)
+
+lemma init_effforcedrole_valid: "erole_functor init_file_forcedrole InheritUpMixed sd = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole  \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"
+by (simp add:erole_func_frole_simp, erule effforcedrole_valid)
+
+lemma init_effinitialrole_valid: "erole_functor init_file_initialrole UseForcedRole sd = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" 
+by (simp add:erole_func_irole_simp, erule effinitialrole_valid)
+
+lemma exec_role_some:
+  "[|sd \<in> init_files; u \<in> init_users|] ==> \<exists> r'. exec_role_aux r sd u = Some r'"
+by (auto simp:exec_role_aux_def split:option.splits t_role.splits 
+        dest!:effirole_sdir_some' efffrole_sdir_some'
+        dest:init_effforcedrole_valid init_effinitialrole_valid
+       intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)
+
+lemma chown_role_some:
+  "u \<in> init_users ==> \<exists> r'. chown_role_aux r fr u = Some r'"
+by (auto simp:chown_role_aux_def split:option.splits t_role.splits 
+        dest!:effirole_sdir_some' efffrole_sdir_some'
+        dest:init_effforcedrole_valid init_effinitialrole_valid
+       intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)
+  
+declare obj2sobj.simps [simp del]
+
+lemma all_sobjs_I:
+  assumes ex: "exists s obj"
+  and vd: "valid s"
+  shows "obj2sobj s obj \<in> all_sobjs"
+using ex vd
+proof (induct s arbitrary:obj)
+  case Nil
+  assume ex:"exists [] obj"
+  show ?case
+  proof (cases obj)
+    case (Proc p) assume prem: "obj = Proc p" 
+    with ex have initp:"p \<in> init_processes" by simp 
+    from initp obtain r where "init_currentrole p = Some r" 
+      using init_proc_has_role by (auto simp:bidirect_in_init_def)  
+    moreover from initp obtain t where "init_process_type p = Some t" 
+      using init_proc_has_type by (auto simp:bidirect_in_init_def)  
+    moreover from initp obtain fr where "init_proc_forcedrole p = Some fr" 
+      using init_proc_has_frole by (auto simp:bidirect_in_init_def)  
+    moreover from initp obtain u where "init_owner p = Some u" 
+      using init_proc_has_owner by (auto simp:bidirect_in_init_def)  
+    ultimately have "obj2sobj [] (Proc p) \<in> all_sobjs" 
+      using initp by (auto intro!:ap_init simp:obj2sobj.simps)
+    with prem show ?thesis by simp
+  next
+    case (File f) assume prem: "obj = File f"
+    with ex have initf: "f \<in> init_files" by simp
+    from initf obtain t where "etype_aux init_file_type_aux f = Some t" 
+      using init_file_has_etype by auto
+    moreover from initf have "source_dir [] f = Some f"
+      by (simp add:source_dir_of_init')
+    ultimately have "obj2sobj [] (File f) \<in> all_sobjs"
+      using initf by (auto simp:etype_of_file_def obj2sobj.simps intro!:af_init)
+    with prem show ?thesis by simp
+  next
+    case (IPC i) assume prem: "obj = IPC i"
+    with ex have initi: "i \<in> init_ipcs" by simp
+    from initi obtain t where "init_ipc_type i = Some t" 
+      using init_ipc_has_type by (auto simp:bidirect_in_init_def)
+    hence "obj2sobj [] (IPC i) \<in> all_sobjs"
+      using initi by (auto intro!:ai_init simp:obj2sobj.simps) 
+    with prem show ?thesis by simp
+  qed
+next
+  case (Cons e s)
+  assume prem: "\<And> obj. \<lbrakk>exists s obj; valid s\<rbrakk> \<Longrightarrow> obj2sobj s obj \<in> all_sobjs"
+    and ex_cons: "exists (e # s) obj" and vs_cons: "valid (e # s)"
+  have vs: "valid s" and rc: "rc_grant s e" and os: "os_grant s e" 
+    using vs_cons by (auto intro:valid_cons valid_os valid_rc)
+  from prem and vs have prem': "\<And> obj. exists s obj \<Longrightarrow> obj2sobj s obj \<in> all_sobjs" by simp
+  show ?case
+  proof (cases e)
+    case (ChangeOwner p u)
+    assume ev: "e = ChangeOwner p u"
+    show ?thesis
+    proof (cases "obj = Proc p")
+      case True 
+      have curp: "p \<in> current_procs s" and exp: "exists s (Proc p)" using os ev by auto
+      from curp obtain r fr t u' srp where sp: "obj2sobj s (Proc p) = SProc (r,fr,t,u') (Some srp)" 
+        using vs apply (drule_tac current_proc_has_sobj, simp) by blast
+      hence sp_in: "SProc (r,fr,t,u') (Some srp) \<in> all_sobjs" using prem' exp by metis
+      have comp: "(r, Proc_type t, CHANGE_OWNER) \<in> compatible" using sp ev rc
+        by (auto simp:obj2sobj.simps split:option.splits)
+      from os ev have uinit: "u \<in> init_users" by simp
+      then obtain nr where chown: "chown_role_aux r fr u = Some nr" 
+        by (auto dest:chown_role_some)
+      hence nsp_in:"obj2sobj (e#s) (Proc p) = SProc (nr,fr,chown_type_aux r nr t, u) (Some srp)" 
+        using sp ev os
+        by (auto split:option.splits t_role.splits 
+          simp del:currentrole.simps type_of_process.simps
+          simp add:chown_role_aux_valid chown_type_aux_valid obj2sobj.simps)
+      thus ?thesis using True ev os rc sp_in sp
+        by (auto simp:chown comp intro!:ap_chown[where u'=u']) 
+    next
+      case False
+      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons
+        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+                              split:option.splits t_role.splits)
+      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+    qed
+  next
+    case (Clone p p')
+    assume ev: "e = Clone p p'"
+    show ?thesis 
+    proof (cases "obj = Proc p'")
+      case True
+      from ev os have exp: "exists s (Proc p)" by (simp add:os_grant.simps)
+      from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)"
+        and srp: "source_proc s p = Some sp" using vs
+        apply (simp del:cp2sproc.simps)
+        by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)
+      hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs
+        by (auto split:option.splits simp add:obj2sobj.simps)
+      have "obj2sobj (e # s) (Proc p') = SProc (r,fr,clone_type_aux r pt, u) (Some sp)"
+        using ev sproc srp vs_cons 
+        by (simp add:obj2sobj.simps cp2sproc_clone del:cp2sproc.simps)
+      thus ?thesis using True SP by (simp add:ap_clone)
+    next
+      case False
+      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons
+        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+                              split:option.splits t_role.splits)
+      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+    qed
+  next
+    case (Execute p f)
+    assume ev: "e = Execute p f"
+    show ?thesis
+    proof (cases "obj = Proc p")
+      case True
+      from ev os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto
+      from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)"
+        and srp: "source_proc s p = Some sp" using vs
+        apply (simp del:cp2sproc.simps)
+        by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)
+      hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs
+        by (auto split:option.splits simp add:obj2sobj.simps)
+      from exf obtain sd t where srdir: "source_dir s f = Some sd" and 
+        etype: "etype_of_file s f = Some t" using vs
+        by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)
+      then obtain srf where SF: "SFile (t, sd) srf \<in> all_sobjs" 
+        using exf prem'[where obj = "File f"] vs
+        by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_file_has_etype)
+      from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs
+        by (auto intro:source_dir_in_init owner_in_users split:option.splits)
+      then obtain nr where "exec_role_aux r sd u = Some nr" by (auto dest:exec_role_some) 
+      
+      hence "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons srdir sproc srp 
+        apply (auto simp:obj2sobj.simps cp2sproc_simps source_proc.simps 
+                   intro:source_dir_in_init simp del:cp2sproc.simps 
+                   split:option.splits dest!:efffrole_sdir_some')
+        apply (rule ap_exec) using SF SP rc ev etype by (auto split:option.splits)
+      with True show ?thesis by simp
+    next
+      case False
+      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons
+        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+                              split:option.splits t_role.splits)
+      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+    qed
+  next
+    case (CreateFile p f)
+    assume ev: "e = CreateFile p f"
+    show ?thesis
+    proof (cases "obj = File f")
+      case True
+      from os ev obtain pf where expf: "exists s (File pf)" and parent:"parent f = Some pf" by auto
+      from expf obtain pft sd srpf where SF: "SFile (pft, sd) srpf \<in> all_sobjs"
+        and eptype: "etype_of_file s pf = Some pft" and srpf: "source_dir s pf = Some sd"
+        using prem'[where obj = "File pf"] vs
+        by (auto split:option.splits if_splits simp:obj2sobj.simps 
+                  dest:current_file_has_etype current_file_has_sd)
+      from os ev have exp: "exists s (Proc p)" by simp
+      then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs"
+        and sproc: "cp2sproc s p = Some (r, fr, pt, u)" 
+        using prem'[where obj = "Proc p"] vs
+        by (auto split:option.splits if_splits simp:obj2sobj.simps 
+                  dest:current_proc_has_sproc)
+      have "obj2sobj (e # s) (File f) \<in> all_sobjs" using ev vs_cons sproc srpf parent os
+        apply (auto simp:obj2sobj.simps source_dir_simps init_notin_curf_deleted  
+                   split:option.splits dest!:current_file_has_etype')
+        apply (case_tac "default_fd_create_type r")
+        using SF SP rc ev eptype sproc
+        apply (rule_tac sf = srpf in af_cfd', auto simp:etype_of_file_def etype_aux_prop3) [1]
+        using SF SP rc ev eptype sproc
+        apply (rule_tac sf = srpf in af_cfd)
+        apply (auto simp:etype_of_file_def etype_aux_prop4)
+        done
+      with True show ?thesis by simp
+    next
+      case False 
+      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps etype_aux_prop2
+                              split:option.splits t_role.splits )
+      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+    qed
+  next
+    case (CreateIPC p i)
+    assume ev: "e = CreateIPC p i"
+    show ?thesis
+    proof (cases "obj = IPC i")
+      case True
+      from os ev have exp: "exists s (Proc p)" by simp
+      then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs"
+        and sproc: "cp2sproc s p = Some (r, fr, pt, u)" 
+        using prem'[where obj = "Proc p"] vs
+        by (auto split:option.splits if_splits simp:obj2sobj.simps 
+                  dest:current_proc_has_sproc)
+      have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os
+        apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
+        apply (rule ai_cipc) using SP sproc rc ev by auto
+      with True show ?thesis by simp
+    next
+      case False 
+      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                              split:option.splits t_role.splits )
+      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+    qed
+  next
+    case (ChangeRole p r')
+    assume ev: "e = ChangeRole p r'"
+    show ?thesis
+    proof (cases "obj = Proc p")
+      case True
+      from os ev have exp: "exists s (Proc p)" by simp
+      then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs"
+        and sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srproc: "source_proc s p = srp"
+        using prem'[where obj = "Proc p"] vs
+        by (auto split:option.splits if_splits simp:obj2sobj.simps 
+                  dest:current_proc_has_sproc)
+      have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os 
+        apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
+        apply (rule ap_crole) using SP sproc rc ev srproc by auto
+      with True show ?thesis by simp
+    next
+      case False 
+      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                              split:option.splits t_role.splits )
+      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+    qed
+  next
+    case (ReadFile p f)
+    assume ev: "e = ReadFile p f"
+    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                            split:option.splits t_role.splits)
+    moreover have "exists s obj" using ev ex_cons
+      by (case_tac obj, auto)
+    ultimately show ?thesis using prem[where obj = obj] vs by simp
+  next
+    case (WriteFile p f)
+    assume ev: "e = WriteFile p f"
+    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                            split:option.splits t_role.splits)
+    moreover have "exists s obj" using ev ex_cons
+      by (case_tac obj, auto)
+    ultimately show ?thesis using prem[where obj = obj] vs by simp
+  next
+    case (Send p i)
+    assume ev: "e = Send p i"
+    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                            split:option.splits t_role.splits)
+    moreover have "exists s obj" using ev ex_cons
+      by (case_tac obj, auto)
+    ultimately show ?thesis using prem[where obj = obj] vs by simp
+  next
+    case (Recv p i)
+    assume ev: "e = Recv p i"
+    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                            split:option.splits t_role.splits)
+    moreover have "exists s obj" using ev ex_cons
+      by (case_tac obj, auto)
+    ultimately show ?thesis using prem[where obj = obj] vs by simp
+  next
+    case (Kill p p')
+    assume ev: "e = Kill p p'"
+    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                            split:option.splits t_role.splits)
+    thus ?thesis using prem[where obj = obj] vs ex_cons ev
+      by (case_tac obj, auto)
+  next
+    case (DeleteFile p f')
+    assume ev: "e = DeleteFile p f'" 
+    have "obj2sobj (e#s) obj = obj2sobj s obj"
+    proof-
+      have "\<And> f. obj = File f ==> obj2sobj (e#s) (File f) = obj2sobj s (File f)"
+        using ev vs os ex_cons vs_cons
+        by (auto simp:obj2sobj.simps etype_of_file_delete source_dir_simps
+                split:option.splits t_role.splits if_splits
+                dest!:current_file_has_etype' current_file_has_sd'
+                 dest:source_dir_prop)
+      moreover have "\<forall> f. obj \<noteq> File f ==> obj2sobj (e#s) obj = obj2sobj s obj"
+        using ev vs_cons ex_cons os vs
+        by (case_tac obj, auto simp:obj2sobj.simps split:option.splits)
+      ultimately show ?thesis by auto
+    qed
+    thus ?thesis using prem[where obj = obj] vs ex_cons ev 
+      by (case_tac obj, auto)
+  next
+    case (DeleteIPC p i)
+    assume ev: "e = DeleteIPC p i"
+    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 
+                            split:option.splits t_role.splits)
+    thus ?thesis using prem[where obj = obj] vs ex_cons ev
+      by (case_tac obj, auto)
+  qed
+qed
+
+declare obj2sobj.simps [simp add]
+
+lemma seeds_in_all_sobjs: 
+  assumes seed: "obj \<in> seeds" shows "init_obj2sobj obj \<in> all_sobjs"
+proof (cases obj)
+  case (Proc p)
+  assume p0: "obj = Proc p" (*?*)
+  from seed p0 have pinit: "p \<in> init_processes" by (drule_tac seeds_in_init, simp)
+  from pinit obtain r where "init_currentrole p = Some r" 
+    using init_proc_has_role by (auto simp:bidirect_in_init_def)
+  moreover from pinit obtain fr where "init_proc_forcedrole p = Some fr"
+    using init_proc_has_frole by (auto simp:bidirect_in_init_def)
+  moreover from pinit obtain pt where "init_process_type p = Some pt"
+    using init_proc_has_type by (auto simp:bidirect_in_init_def)
+  moreover from pinit obtain u where "init_owner p = Some u"
+    using init_proc_has_owner by (auto simp:bidirect_in_init_def)
+  ultimately show ?thesis using p0 by (auto intro:ap_init)
+next
+  case (File f) 
+  assume p0: "obj = File f" (*?*)
+  from seed p0 have finit: "f \<in> init_files" by (drule_tac seeds_in_init, simp)
+  then obtain t where "etype_aux init_file_type_aux f = Some t"
+    by (auto dest:init_file_has_etype)
+  with finit p0 show ?thesis by (auto intro:af_init)
+next
+  case (IPC i)
+  assume p0: "obj = IPC i" (*?*)
+  from seed p0 have iinit: "i \<in> init_ipcs" by (drule_tac seeds_in_init, simp)
+  then obtain t where "init_ipc_type i = Some t" using init_ipc_has_type
+    by (auto simp:bidirect_in_init_def)
+  with iinit p0 show ?thesis by (auto intro:ai_init)
+qed
+
+lemma tainted_s_in_all_sobjs:
+  "sobj \<in> tainted_s \<Longrightarrow> sobj \<in> all_sobjs"
+apply (erule tainted_s.induct)
+apply (erule seeds_in_all_sobjs)
+apply (auto intro:ap_crole ap_exec ap_chown ai_cipc af_cfd af_cfd' ap_clone)
+done
+
+end
+
+context tainting_s_sound begin
+
+(*** all_sobjs' equal with all_sobjs in the view of soundness ***)
+
+lemma all_sobjs'_eq1: "sobj \<in> all_sobjs \<Longrightarrow> sobj \<in> all_sobjs'"
+apply (erule all_sobjs.induct)
+apply (auto intro:af'_init af'_cfd af'_cfd' ai'_init ai'_cipc ap'_init ap'_crole ap'_exec ap'_chown)
+by (simp add:clone_type_aux_def clone_type_unchange)
+
+lemma all_sobjs'_eq2: "sobj \<in> all_sobjs' \<Longrightarrow> sobj \<in> all_sobjs"
+apply (erule all_sobjs'.induct)
+by (auto intro:af_init af_cfd af_cfd' ai_init ai_cipc ap_init ap_crole ap_exec ap_chown)
+
+lemma all_sobjs'_eq: "(sobj \<in> all_sobjs) = (sobj \<in> all_sobjs')"
+by (auto intro:iffI all_sobjs'_eq1 all_sobjs'_eq2)
+
+(************************ all_sobjs Elim Rules ********************)
+
+declare obj2sobj.simps [simp del]
+declare cp2sproc.simps [simp del]
+
+lemma all_sobjs_E0_aux[rule_format]:
+  "sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> no_del_event s' \<and> initp_intact s' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj))"
+proof (induct rule:all_sobjs'.induct)
+  case (af'_init f t) show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+      and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+      and exso': "exists s' obj'"
+    from nodels' af'_init(1) have exf: "f \<in> current_files s'" 
+      by (drule_tac obj = "File f" in nodel_imp_exists, simp+)    
+    have "obj2sobj s' (File f) = SFile (t, f) (Some f)"
+    proof-
+      have "obj2sobj [] (File f) = SFile (t, f) (Some f)"  using af'_init 
+        by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps
+                split:option.splits)
+      thus ?thesis using vss' exf nodels' af'_init(1) 
+        by (drule_tac obj2sobj_file_remains_app', auto)
+    qed
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+             obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)
+      by (simp add:vss' sobjs' nodels' intacts' exf exso')
+  qed
+next
+  case (af'_cfd t sd srf r fr pt u srp t') 
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"
+    with af'_cfd(1,2) obtain sa pf where
+      "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+      "exists (sa@s') obj'" and "initp_intact (sa@s')" and
+      SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+      exfa: "pf \<in> current_files (sa@s')" 
+      apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+      by (frule obj2sobj_file, auto)
+    with af'_cfd(3,4) notUkn obtain sb p where
+      SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+      soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 
+      exsoab: "exists (sb@sa@s') obj'" and
+      intactab: "initp_intact (sb@sa@s')" and
+      nodelab: "no_del_event (sb@sa@s')"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+      apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+    obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 
+      and tau: "\<tau>=sb@sa@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau af'_cfd(5,6,7) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+                split:if_splits option.splits t_rc_file_type.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+      by (simp_all add:initp_intact_I_others)  moreover
+    have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+    proof-
+      have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+        using ev tau SFab SPab af'_cfd(5)
+        by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def
+          split:option.splits if_splits  intro!:etype_aux_prop4)
+      moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+        using ev tau SFab SPab valid ncf_parent
+        by (auto simp:source_dir_simps obj2sobj.simps 
+                split:if_splits option.splits)
+      ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]
+        nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+        by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+    qed
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+      obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj "
+      using tau ev
+      by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+)
+  qed
+next
+  case (af'_cfd' t sd srf r fr pt u srp)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"
+    with af'_cfd'(1,2) obtain sa pf where
+      "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+      "exists (sa@s') obj'" and "initp_intact (sa@s')" and
+      SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+      exfa: "pf \<in> current_files (sa@s')" 
+      apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+      by (frule obj2sobj_file, auto)
+    with af'_cfd'(3,4) notUkn obtain sb p where
+      SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+      soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 
+      exsoab: "exists (sb@sa@s') obj'" and
+      intactab: "initp_intact (sb@sa@s')" and
+      nodelab: "no_del_event (sb@sa@s')"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+      apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+    obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 
+      and tau: "\<tau>=sb@sa@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau af'_cfd'(5,6) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+                split:if_splits option.splits t_rc_file_type.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+      by (simp add:initp_intact_I_others)  moreover
+    have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+    proof-
+      have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+      proof-
+        have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+          using ev tau SPab af'_cfd'(5) 
+          by (auto simp:obj2sobj.simps ncf_parent etype_of_file_def cp2sproc.simps
+            split:option.splits   intro!:etype_aux_prop3)
+        thus ?thesis using SFab tau ev
+          by (auto simp:obj2sobj.simps split:option.splits if_splits)
+      qed
+      moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+        using ev tau SFab SPab valid ncf_parent
+        by (auto simp:source_dir_simps obj2sobj.simps 
+                split:if_splits option.splits)
+      ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]
+        nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+        by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+    qed
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+      obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj"
+      using tau ev
+      by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+)
+  qed 
+next
+  case (ai'_init i t) 
+  hence initi: "i \<in> init_ipcs" using init_ipc_has_type
+    by (simp add:bidirect_in_init_def)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+      and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+      and exso': "exists s' obj'"
+    from nodels' initi have exi: "i \<in> current_ipcs s'" 
+      by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+)    
+    have "obj2sobj s' (IPC i) = SIPC t (Some i)"
+    proof-
+      have "obj2sobj [] (IPC i) = SIPC t (Some i)"  
+        using ai'_init initi by (auto simp:obj2sobj.simps)
+      thus ?thesis using vss' exi nodels' initi 
+        by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps)
+    qed
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+             obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI)
+      by (simp add:vss' sobjs' nodels' exi exso' intacts' del:obj2sobj.simps)
+  qed
+next
+  case (ai'_cipc r fr pt u srp)
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"
+    with ai'_cipc(1,2) notUkn obtain s p where
+      SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and
+      soab: "obj2sobj (s@s') obj' = sobj'" and 
+      exsoab: "exists (s@s') obj'" and
+      intactab: "initp_intact (s@s')" and
+      nodelab: "no_del_event (s@s')"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ai'_cipc(3) SPab
+        by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+      by (simp add:initp_intact_I_others)  moreover
+    have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None"
+      using ev tau SPab nodel 
+        nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>]
+      by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps 
+              split:option.splits  dest:no_del_event_cons_D)
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+      obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj"
+      using tau ev
+      by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, simp+)
+  qed 
+next
+  case (ap'_init p r fr t u)
+  hence initp: "p \<in> init_processes" using init_proc_has_role
+    by (simp add:bidirect_in_init_def)
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'"
+      and Nodels': "no_del_event s'"and Intacts':"initp_intact s'"
+      and exso': "exists s' obj'"
+    from Nodels' initp have exp: "p \<in> current_procs s'" 
+      apply (drule_tac obj = "Proc p" in nodel_imp_un_deleted)
+      by (drule not_deleted_imp_exists, simp+)
+    with Intacts' initp ap'_init have "obj2sobj s' (Proc p) = SProc (r, fr, t, u) (Some p)"
+      by (auto simp:initp_intact_def split:option.splits)
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+             obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p" in exI)
+      by (simp add:VSs' SOs' Nodels' exp exso' initp intact_imp_butp Intacts'
+               del:obj2sobj.simps)
+  qed
+next
+  case (ap'_crole r fr t u srp r')
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_crole(1,2) obtain s p where
+      VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+      and nodelab: "no_del_event (s@s')"
+      and intactab: "initp_intact (s@s')"
+      and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+      and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = ChangeRole (new_proc (s@s')) r'" 
+      and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_crole(3) SPab 
+        by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact (e#\<tau>)" using tau ev intactab valid
+      by (simp add:initp_intact_I_crole)   moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+      by (case_tac obj', simp+)  moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by (auto)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by auto
+      moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+        apply (case_tac "p' = new_proc (s @ s')") 
+        using vs_tau exobj'ab tau
+        apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+        using tau ev SOab' valid notUkn vs_tau
+        by (auto simp:obj2sobj.simps cp2sproc_simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (r', fr, t, u) srp"
+      using SPab tau vs_tau ev valid
+      by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+              split:option.splits)  moreover
+    have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp  
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 
+      obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj"
+      using ev tau
+      apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+      by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+  qed
+next
+  case (ap'_chown r fr t u srp u' nr)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_chown(1,2) obtain s p where
+      VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+      and nodelab: "no_del_event (s@s')" and intactab: "initp_intact (s@s')"
+      and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+      and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = ChangeOwner (new_proc (s@s')) u'" 
+      and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp ap'_chown(3) by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_chown(5) SPab 
+        by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+                split:option.splits t_rc_proc_type.splits)
+          (* here is another place of no_limit of clone event assumption *)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact (e#\<tau>)" using intactab tau ev valid 
+      by (simp add:initp_intact_I_chown)  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+      by (case_tac obj', simp+)  moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by (auto)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by auto
+      moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+        apply (case_tac "p' = new_proc (s @ s')") 
+        using vs_tau exobj'ab tau
+        apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+        using tau ev SOab' valid notUkn vs_tau 
+        by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = 
+          SProc (nr,fr,chown_type_aux r nr t,u') srp"
+      using SPab tau vs_tau ev valid ap'_chown(4)
+      by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+              split:option.splits)  moreover
+    have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp   moreover 
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 
+      obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and>
+      exists (s @ s') obj"
+      using ev tau
+      apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+      by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+  qed
+next
+  case (ap'_exec r fr pt u sp t sd sf r' fr')
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_exec(3,4) obtain sa f where
+      SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and
+      Exfa: "exists (sa @ s') (File f)" and 
+      butsa: "initp_intact (sa @ s')" and
+      othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> 
+               exists (sa @s') obj' \<and> no_del_event (sa @ s')" 
+      by (blast dest:obj2sobj_file intro:nodel_exists_remains)
+    with ap'_exec(1,2) notUkn obtain sb p where
+      VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'"
+      and nodelab: "no_del_event (sb@sa@s')"
+      and intactab: "initp_intact (sb@sa@s')"
+      and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp"
+      and exp:"exists (sb@sa@s') (Proc p)" and exobj'ab:"exists (sb@sa@s') obj'"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = Execute (new_proc (sb@sa@s')) f" 
+      and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+    from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')" 
+      apply (drule_tac obj = "File f" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp by (simp add:exf)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_exec(5) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+                split:if_splits option.splits)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact (e#\<tau>)" using tau ev intactab valid
+      by (simp add:initp_intact_I_exec)  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+      by (case_tac obj', simp+) moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+        by (auto simp del:obj2sobj.simps)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+        by (auto simp del:obj2sobj.simps)
+      moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+        apply (case_tac "p' = new_proc (sb @ sa @ s')") 
+        using vs_tau exobj'ab tau
+        apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+        using tau ev SOab' valid notUkn vs_tau 
+        by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc (new_proc (sb @ sa @ s'))) = 
+          SProc (r',fr',exec_type_aux r pt, u) sp"
+    proof-
+      have "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau
+        by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+      hence "obj2sobj \<tau> (Proc (new_proc (sb@sa@s'))) = SProc (r,fr,pt,u) sp" using tau
+      by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange 
+              split:option.splits)
+      moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau 
+        by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+      ultimately show ?thesis using valid ev ap'_exec(6,7) 
+        by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+    qed 
+    ultimately 
+    show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 
+      obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and>
+      exists (s @ s') obj"
+      using ev tau
+      apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI)
+      by (rule_tac x = "Proc (new_proc (sb @ sa @ s'))" in exI, auto)
+  qed
+qed
+
+(* this is for ts2t createfile case ... *)
+lemma all_sobjs_E0:
+  "\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown; 
+    no_del_event s'; initp_intact s'\<rbrakk>
+   \<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and>
+                no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 
+                obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj"
+by (drule all_sobjs_E0_aux, auto)
+
+lemma all_sobjs_E1_aux[rule_format]:
+  "sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> no_del_event s' \<and> initp_intact_but s' sobj' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj))"
+proof (induct rule:all_sobjs'.induct)
+  case (af'_init f t) show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+      and nodels': "no_del_event s'"and intacts':"initp_intact_but s' sobj'"
+      and exso': "exists s' obj'"
+    from nodels' af'_init(1) have exf: "f \<in> current_files s'" 
+      by (drule_tac obj = "File f" in nodel_imp_exists, simp+)    
+    have "obj2sobj s' (File f) = SFile (t, f) (Some f)"
+    proof-
+      have "obj2sobj [] (File f) = SFile (t, f) (Some f)"  using af'_init 
+        by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps
+                split:option.splits)
+      thus ?thesis using vss' exf nodels' af'_init(1) 
+        by (drule_tac obj2sobj_file_remains_app', auto)
+    qed
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+             obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)
+      by (simp add:vss' sobjs' nodels' intacts' exf exso')
+  qed
+next
+  case (af'_cfd t sd srf r fr pt u srp t') 
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" 
+      and exobj':"exists s' obj'"
+    with af'_cfd(1,2) obtain sa pf where
+      "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+      "exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and
+      SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+      exfa: "pf \<in> current_files (sa@s')" 
+      apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+      by (frule obj2sobj_file, auto)
+    with af'_cfd(3,4) notUkn obtain sb p where
+      SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+      soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 
+      exsoab: "exists (sb@sa@s') obj'" and
+      intactab: "initp_intact_but (sb@sa@s') sobj'" and
+      nodelab: "no_del_event (sb@sa@s')"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+      apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+    obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 
+      and tau: "\<tau>=sb@sa@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau af'_cfd(5,6,7) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+                split:if_splits option.splits t_rc_file_type.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps' 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+    proof-
+      have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+        using ev tau SFab SPab af'_cfd(5)
+        by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def
+          split:option.splits if_splits  intro!:etype_aux_prop4)
+      moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+        using ev tau SFab SPab valid ncf_parent
+        by (auto simp:source_dir_simps obj2sobj.simps 
+                split:if_splits option.splits)
+      ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]
+        nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+        by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+    qed  moreover
+    have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel
+        apply (case_tac sobj', case_tac option)
+        by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)  
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+      obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj "
+      using tau ev
+      apply (rule_tac x = "e#sb@sa" in exI)
+      by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+  qed
+next
+  case (af'_cfd' t sd srf r fr pt u srp)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" 
+      and exobj':"exists s' obj'"
+    with af'_cfd'(1,2) obtain sa pf where
+      "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+      "exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and
+      SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+      exfa: "pf \<in> current_files (sa@s')" 
+      apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+      by (frule obj2sobj_file, auto)
+    with af'_cfd'(3,4) notUkn obtain sb p where
+      SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+      soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 
+      exsoab: "exists (sb@sa@s') obj'" and
+      intactab: "initp_intact_but (sb@sa@s') sobj'" and
+      nodelab: "no_del_event (sb@sa@s')"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+      apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+    obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 
+      and tau: "\<tau>=sb@sa@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau af'_cfd'(5,6) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+                split:if_splits option.splits t_rc_file_type.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps' 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+    proof-
+      have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+      proof-
+        have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+          using ev tau SPab af'_cfd'(5) 
+          by (auto simp:obj2sobj.simps cp2sproc.simps ncf_parent etype_of_file_def
+            split:option.splits   intro!:etype_aux_prop3)
+        thus ?thesis using SFab tau ev
+          by (auto simp:obj2sobj.simps split:option.splits if_splits)
+      qed
+      moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+        using ev tau SFab SPab valid ncf_parent
+        by (auto simp:source_dir_simps obj2sobj.simps 
+                split:if_splits option.splits)
+      ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]
+        nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+        by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+    qed  moreover
+    have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel
+        apply (case_tac sobj', case_tac option)
+        by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)  
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+      obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj"
+      using tau ev
+      apply (rule_tac x = "e#sb@sa" in exI)
+      by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+  qed 
+next
+  case (ai'_init i t) 
+  hence initi: "i \<in> init_ipcs" using init_ipc_has_type
+    by (simp add:bidirect_in_init_def)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+      and nodels': "no_del_event s'"and intacts':"initp_intact_but s' sobj'"
+      and exso': "exists s' obj'"
+    from nodels' initi have exi: "i \<in> current_ipcs s'" 
+      by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+)    
+    have "obj2sobj s' (IPC i) = SIPC t (Some i)"
+    proof-
+      have "obj2sobj [] (IPC i) = SIPC t (Some i)"  
+        using ai'_init initi by (auto simp:obj2sobj.simps)
+      thus ?thesis using vss' exi nodels' initi 
+        by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps)
+    qed
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+             obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI)
+      by (simp add:vss' sobjs' nodels' exi exso' intacts' del:obj2sobj.simps)
+  qed
+next
+  case (ai'_cipc r fr pt u srp)
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" 
+      and exobj':"exists s' obj'"
+    with ai'_cipc(1,2) notUkn obtain s p where
+      SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and
+      soab: "obj2sobj (s@s') obj' = sobj'" and 
+      exsoab: "exists (s@s') obj'" and
+      intactab: "initp_intact_but (s@s') sobj'" and
+      nodelab: "no_del_event (s@s')"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ai'_cipc(3) SPab
+        by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps' 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None"
+      using ev tau SPab nodel 
+        nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>]
+      by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps 
+              split:option.splits dest:no_del_event_cons_D)  moreover
+    have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel
+        apply (case_tac sobj', case_tac option)
+        by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)  
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+      obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj"
+      using tau ev
+      by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, auto)
+  qed 
+next
+  case (ap'_init p r fr t u)  (* the big difference from other elims is in this case *)
+  hence initp: "p \<in> init_processes" using init_proc_has_role
+    by (simp add:bidirect_in_init_def)
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'"
+      and Nodels': "no_del_event s'"and Intacts':"initp_intact_but s' sobj'"
+      and exso': "exists s' obj'" and notUkn: "sobj' \<noteq> Unknown"
+    from Nodels' initp have exp: "p \<in> current_procs s'" 
+      by (drule_tac obj = "Proc p" in nodel_imp_exists, simp+)
+    have "\<exists> p'. obj2sobj s' (Proc p') = SProc (r,fr,t,u) (Some p) \<and> p' \<in> current_procs s'"
+    proof (cases sobj')
+      case (SProc sp srp)
+      show ?thesis
+      proof (cases srp)
+        case None
+        with SProc Intacts' have "initp_intact s'" by simp
+        thus ?thesis using initp ap'_init
+          apply (rule_tac x = p in exI)
+          by (auto simp:initp_intact_def exp split:option.splits)
+      next
+        case (Some p')
+        show ?thesis
+        proof (cases "p' = p")
+          case True
+          with Intacts' SProc Some have "initp_alter s' p" 
+            by (simp add:initp_intact_butp_def)
+          then obtain pa where "pa \<in> current_procs s'"
+            and "obj2sobj s' (Proc pa) = init_obj2sobj (Proc p)"
+            by (auto simp only:initp_alter_def)
+          thus ?thesis using ap'_init initp 
+            by (rule_tac x = pa in exI, auto)
+        next
+          case False
+          with Intacts' SProc Some initp
+          have "obj2sobj s' (Proc p) = init_obj2sobj (Proc p)"
+            apply (simp only:initp_intact_butp_def initp_intact_but.simps)
+            by (erule conjE, erule_tac x = p in allE, simp)
+          thus ?thesis using ap'_init exp
+            by (rule_tac x = p in exI, auto split:option.splits)
+        qed
+      qed
+    next
+      case (SFile sf srf)
+      thus ?thesis using ap'_init exp Intacts' initp
+        by (rule_tac x = p in exI, auto split:option.splits simp:initp_intact_def)
+    next
+      case (SIPC si sri)
+      thus ?thesis using ap'_init exp Intacts' initp
+        by (rule_tac x = p in exI, auto split:option.splits simp:initp_intact_def)
+    next
+      case Unknown
+      thus ?thesis using notUkn by simp
+    qed
+    then obtain p' where "obj2sobj s' (Proc p') = SProc (r, fr, t, u) (Some p)"
+      and "p' \<in> current_procs s'" by blast
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+             obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p'" in exI)
+      by (simp add:VSs' SOs' Nodels' exp exso' Intacts') 
+  qed 
+next
+  case (ap'_crole r fr t u srp r')
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_crole(1,2) obtain s p where
+      VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+      and nodelab: "no_del_event (s@s')"
+      and intactab: "initp_intact_but (s@s') sobj'"
+      and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+      and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = ChangeRole (new_proc (s@s')) r'" 
+      and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+    have np_not_initp: "new_proc (s@s') \<notin> init_processes" using nodelab 
+      apply (rule_tac notI, drule_tac obj = "Proc (new_proc (s@s'))" in nodel_imp_exists)
+      by (auto simp:np_notin_curp)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_crole(3) SPab 
+        by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact_but (e#\<tau>) sobj'"
+    proof (cases sobj')
+      case (SProc sp srp)
+      show ?thesis
+      proof (cases srp)
+        case (Some p')
+        with SOab' exobj'ab VSab intactab notUkn SProc
+        have butp: "p' \<in> init_processes \<and> initp_intact_butp (s@s') p'"
+          by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps
+                                split:if_splits option.splits)
+        then obtain p'' where exp': "p'' \<in> current_procs (s@s')" and 
+          SP': "obj2sobj (s@s') (Proc p'') = init_obj2sobj (Proc p')"
+          by (auto simp:initp_alter_def initp_intact_butp_def)
+        hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel
+          apply (simp add:initp_alter_def del:init_obj2sobj.simps)
+          apply (rule_tac x = p'' in exI, rule conjI, simp)
+          apply (subgoal_tac "p'' \<noteq> new_proc (s @s')")
+          apply (auto simp:obj2sobj.simps cp2sproc.simps 
+                  simp del:init_obj2sobj.simps  split:option.splits)[1]
+          by (rule notI, simp add:np_notin_curp)
+        thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp
+          apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps)
+          apply (rule impI|rule allI|rule conjI|erule conjE)+
+          apply (erule_tac x = pa in allE)
+          by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps
+                  split:option.splits)
+      next
+        case None
+        with intactab SProc 
+        have "initp_intact (s@s')" by simp
+        hence "initp_intact (e#\<tau>)" using tau ev valid
+          by (simp add:initp_intact_I_crole)
+        thus ?thesis using SProc None by simp
+      qed
+    next
+      case (SFile sf srf)
+      with intactab SFile
+      have "initp_intact (s@s')" by simp
+      hence "initp_intact (e#\<tau>)" using tau ev valid
+        by (simp add:initp_intact_I_crole)
+      thus ?thesis using SFile by simp
+    next
+      case (SIPC si sri)
+      with intactab SIPC
+      have "initp_intact (s@s')" by simp
+      hence "initp_intact (e#\<tau>)" using tau ev valid
+        by (simp add:initp_intact_I_crole)
+      thus ?thesis using SIPC by simp
+    next
+      case Unknown 
+      with notUkn show ?thesis by simp
+    qed  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+      by (case_tac obj', simp+)  moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by (auto)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by auto
+      moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+        apply (case_tac "p' = new_proc (s @ s')") 
+        using vs_tau exobj'ab tau
+        apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+        using tau ev SOab' valid notUkn vs_tau 
+        by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (r', fr, t, u) srp"
+      using SPab tau vs_tau ev valid
+      by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+              split:option.splits)  moreover
+    have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp  
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> 
+      obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj"
+      using ev tau
+      apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+      by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+  qed 
+next
+  case (ap'_chown r fr t u srp u' nr)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_chown(1,2) obtain s p where
+      VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+      and nodelab: "no_del_event (s@s')" and intactab: "initp_intact_but (s@s') sobj'"
+      and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+      and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = ChangeOwner (new_proc (s@s')) u'" 
+      and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+    have np_not_initp: "new_proc (s@s') \<notin> init_processes" using nodelab 
+      apply (rule_tac notI, drule_tac obj = "Proc (new_proc (s@s'))" in nodel_imp_exists)
+      by (auto simp:np_notin_curp)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp ap'_chown(3) by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_chown(5) SPab 
+        by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+                split:option.splits t_rc_proc_type.splits)
+          (* here is another place of no_limit of clone event assumption *)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact_but (e#\<tau>) sobj'"
+    proof (cases sobj')
+      case (SProc sp srp)
+      show ?thesis
+      proof (cases srp)
+        case (Some p')
+        with SOab' exobj'ab VSab intactab notUkn SProc
+        have butp: "p' \<in> init_processes \<and> initp_intact_butp (s@s') p'"
+          by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps
+                                split:if_splits option.splits)
+        then obtain p'' where exp': "p'' \<in> current_procs (s@s')" and 
+          SP': "obj2sobj (s@s') (Proc p'') = init_obj2sobj (Proc p')"
+          by (auto simp:initp_alter_def initp_intact_butp_def)
+        hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel
+          apply (simp add:initp_alter_def del:init_obj2sobj.simps)
+          apply (rule_tac x = p'' in exI, rule conjI, simp)
+          apply (subgoal_tac "p'' \<noteq> new_proc (s @s')")
+          apply (auto simp:obj2sobj.simps cp2sproc.simps 
+                  simp del:init_obj2sobj.simps  split:option.splits)[1]
+          by (rule notI, simp add:np_notin_curp)
+        thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp
+          apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps)
+          apply (rule impI|rule allI|rule conjI|erule conjE)+
+          apply (erule_tac x = pa in allE)
+          by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps
+                  split:option.splits)
+      next
+        case None
+        with intactab SProc 
+        have "initp_intact (s@s')" by simp
+        hence "initp_intact (e#\<tau>)" using tau ev valid
+          by (simp add:initp_intact_I_chown)
+        thus ?thesis using SProc None by simp
+      qed
+    next
+      case (SFile sf srf)
+      with intactab SFile
+      have "initp_intact (s@s')" by simp
+      hence "initp_intact (e#\<tau>)" using tau ev valid
+        by (simp add:initp_intact_I_chown)
+      thus ?thesis using SFile by simp
+    next
+      case (SIPC si sri)
+      with intactab SIPC
+      have "initp_intact (s@s')" by simp
+      hence "initp_intact (e#\<tau>)" using tau ev valid
+        by (simp add:initp_intact_I_chown)
+      thus ?thesis using SIPC by simp
+    next
+      case Unknown 
+      with notUkn show ?thesis by simp
+    qed  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+      by (case_tac obj', simp+)  moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by (auto)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by auto
+      moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+        apply (case_tac "p' = new_proc (s @ s')") 
+        using vs_tau exobj'ab tau
+        apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+        using tau ev SOab' valid notUkn vs_tau 
+        by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = 
+          SProc (nr,fr,chown_type_aux r nr t,u') srp"
+      using SPab tau vs_tau ev valid ap'_chown(4)
+      by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+              split:option.splits)  moreover
+    have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp   moreover 
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> 
+      obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and>
+      exists (s @ s') obj"
+      using ev tau
+      apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+      by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+  qed
+next
+  case (ap'_exec r fr pt u sp t sd sf r' fr')
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_exec(3,4) obtain sa f where
+      SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and
+      Exfa: "exists (sa @ s') (File f)" and 
+      butsa: "initp_intact_but (sa @ s') sobj'" and
+      othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> 
+               exists (sa @s') obj' \<and> no_del_event (sa @ s')" 
+      by (blast dest:obj2sobj_file intro:nodel_exists_remains)
+    with ap'_exec(1,2) notUkn obtain sb p where
+      VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'"
+      and nodelab: "no_del_event (sb@sa@s')"
+      and intactab: "initp_intact_but (sb@sa@s') sobj'"
+      and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp"
+      and exp:"exists (sb@sa@s') (Proc p)" and exobj'ab:"exists (sb@sa@s') obj'"
+      by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = Execute (new_proc (sb@sa@s')) f" 
+      and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+    from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')" 
+      apply (drule_tac obj = "File f" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all)
+    have np_not_initp: "new_proc (sb@sa@s') \<notin> init_processes" using nodelab 
+      apply (rule_tac notI, drule_tac obj = "Proc (new_proc (sb@sa@s'))" in nodel_imp_exists)
+      by (auto simp:np_notin_curp)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp by (simp add:exf)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_exec(5) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+                split:if_splits option.splits)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact_but (e#\<tau>) sobj'"
+    proof (cases sobj')
+      case (SProc sp srp)
+      show ?thesis
+      proof (cases srp)
+        case (Some p')
+        with SOab' exobj'ab VSab intactab notUkn SProc
+        have butp: "p' \<in> init_processes \<and> initp_intact_butp (sb@sa@s') p'"
+          by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps
+                                split:if_splits option.splits)
+        then obtain p'' where exp': "p'' \<in> current_procs (sb@sa@s')" and 
+          SP': "obj2sobj (sb@sa@s') (Proc p'') = init_obj2sobj (Proc p')"
+          by (auto simp:initp_alter_def initp_intact_butp_def)
+        hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel
+          apply (simp add:initp_alter_def del:init_obj2sobj.simps)
+          apply (rule_tac x = p'' in exI, rule conjI, simp)
+          apply (subgoal_tac "p'' \<noteq> new_proc (sb@sa@s')")
+          apply (auto simp:obj2sobj.simps cp2sproc.simps 
+                  simp del:init_obj2sobj.simps  split:option.splits)[1]
+          by (rule notI, simp add:np_notin_curp)
+        thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp
+          apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps)
+          apply (rule impI|rule allI|rule conjI|erule conjE)+
+          apply (erule_tac x = pa in allE)
+          by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps
+                  split:option.splits)
+      next
+        case None
+        with intactab SProc 
+        have "initp_intact (sb@sa@s')" by simp
+        hence "initp_intact (e#\<tau>)" using tau ev valid
+          by (simp add:initp_intact_I_exec)
+        thus ?thesis using SProc None by simp
+      qed
+    next
+      case (SFile sf srf)
+      with intactab SFile
+      have "initp_intact (sb@sa@s')" by simp
+      hence "initp_intact (e#\<tau>)" using tau ev valid
+        by (simp add:initp_intact_I_exec)
+      thus ?thesis using SFile by simp
+    next
+      case (SIPC si sri)
+      with intactab SIPC
+      have "initp_intact (sb@sa@s')" by simp
+      hence "initp_intact (e#\<tau>)" using tau ev valid
+        by (simp add:initp_intact_I_exec)
+      thus ?thesis using SIPC by simp
+    next
+      case Unknown 
+      with notUkn show ?thesis by simp
+    qed  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+      by (case_tac obj', simp+) moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+        by (auto simp del:obj2sobj.simps)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+        by (auto simp del:obj2sobj.simps)
+      moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+        apply (case_tac "p' = new_proc (sb @ sa @ s')") 
+        using vs_tau exobj'ab tau
+        apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+        using tau ev SOab' valid notUkn vs_tau 
+        by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc (new_proc (sb @ sa @ s'))) = 
+          SProc (r',fr',exec_type_aux r pt, u) sp"
+    proof-
+      have "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau
+        by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+      hence "obj2sobj \<tau> (Proc (new_proc (sb@sa@s'))) = SProc (r,fr,pt,u) sp" using tau
+      by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange 
+              split:option.splits)
+      moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau 
+        by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+      ultimately show ?thesis using valid ev ap'_exec(6,7) 
+        by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+    qed 
+    ultimately  show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> 
+      obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and>
+      exists (s @ s') obj"
+      using ev tau
+      apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI)
+      by (rule_tac x = "Proc (new_proc (sb @ sa @ s'))" in exI, auto)
+  qed
+qed
+
+(* this is for all_sobjs_E2 *)
+lemma all_sobjs_E1:
+  "\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown; 
+    no_del_event s'; initp_intact_but s' sobj'\<rbrakk>
+   \<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>  exists (s@s') obj \<and>
+                no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> 
+                obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj"
+by (drule all_sobjs_E1_aux, auto)
+
+
+lemma all_sobjs_E2_aux[rule_format]:
+  "sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> not_both_sproc sobj sobj' \<and> no_del_event s' \<and> initp_intact s' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj \<and> sobj_source_eq_obj sobj obj))"
+proof (induct rule:all_sobjs'.induct)
+  case (af'_init f t) show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+      and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+      and notboth: "not_both_sproc (SFile (t, f) (Some f)) sobj'"
+      and exso': "exists s' obj'"
+    from nodels' af'_init(1) have exf: "f \<in> current_files s'" 
+      by (drule_tac obj = "File f" in nodel_imp_exists, simp+)    
+    have "obj2sobj s' (File f) = SFile (t, f) (Some f)"
+    proof-
+      have "obj2sobj [] (File f) = SFile (t, f) (Some f)"  using af'_init 
+        by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps
+                split:option.splits)
+      thus ?thesis using vss' exf nodels' af'_init(1) 
+        by (drule_tac obj2sobj_file_remains_app', auto)
+    qed
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+             initp_intact_but (s @ s') (SFile (t, f) (Some f)) \<and>
+             obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and>
+             exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t, f) (Some f)) obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)
+      by (simp add:vss' sobjs' nodels' intacts' exf exso')
+  qed
+next
+  case (af'_cfd t sd srf r fr pt u srp t') 
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and Both:"not_both_sproc (SFile (t', sd) None) sobj'"
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" 
+      and exobj':"exists s' obj'"
+    with af'_cfd(1,2) obtain sa pf where
+      "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+      "exists (sa@s') obj'" and "initp_intact (sa@s')" and
+      SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+      exfa: "pf \<in> current_files (sa@s')" 
+      apply (drule_tac sf' = "(t, sd)" and srf' = srf in not_both_I_file)
+      apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+      by (frule obj2sobj_file, auto)
+    with af'_cfd(3) notUkn obtain sb p where
+      SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+      soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 
+      exsoab: "exists (sb@sa@s') obj'" and
+      intactab: "initp_intact (sb@sa@s')" and
+      nodelab: "no_del_event (sb@sa@s')"
+      apply (drule_tac s'= "sa@s'" and obj' = obj' in all_sobjs_E0, auto) 
+      apply (frule obj2sobj_proc, erule exE)
+      by (auto intro:nodel_exists_remains)
+    from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+      apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+    obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 
+      and tau: "\<tau>=sb@sa@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau af'_cfd(5,6,7) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+                split:if_splits option.splits t_rc_file_type.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps' 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+      by (simp add:initp_intact_I_others)  moreover
+    have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+    proof-
+      have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+        using ev tau SFab SPab af'_cfd(5)
+        by (auto simp:obj2sobj.simps etype_of_file_def cp2sproc.simps
+          split:option.splits if_splits  intro!:etype_aux_prop4)
+      moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+        using ev tau SFab SPab valid ncf_parent
+        by (auto simp:source_dir_simps obj2sobj.simps 
+                split:if_splits option.splits)
+      ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]
+        nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+        by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+    qed
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+      initp_intact_but (s @ s') (SFile (t', sd) None) \<and>
+      obj2sobj (s @ s') obj = SFile (t', sd) None \<and>
+      exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t', sd) None) obj"
+      using tau ev
+      apply (rule_tac x = "e#sb@sa" in exI)
+      by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+  qed
+next
+  case (af'_cfd' t sd srf r fr pt u srp)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and Both:"not_both_sproc (SFile (t, sd) None) sobj'"
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" 
+      and exobj':"exists s' obj'"
+    with af'_cfd'(1,2) obtain sa pf where
+      "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+      "exists (sa@s') obj'" and "initp_intact (sa@s')" and
+      SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+      exfa: "pf \<in> current_files (sa@s')" 
+      apply (drule_tac sf' = "(t, sd)" and srf' = srf in not_both_I_file)
+      apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+      by (frule obj2sobj_file, auto)
+    with af'_cfd'(3) notUkn obtain sb p where
+      SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+      soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 
+      exsoab: "exists (sb@sa@s') obj'" and
+      intactab: "initp_intact (sb@sa@s')" and
+      nodelab: "no_del_event (sb@sa@s')"
+      apply (drule_tac s'= "sa@s'" and obj' = obj' in all_sobjs_E0, auto) 
+      apply (frule obj2sobj_proc, erule exE)
+      by (auto intro:nodel_exists_remains)
+    from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+      apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+    obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 
+      and tau: "\<tau>=sb@sa@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau af'_cfd'(5,6) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+                split:if_splits option.splits t_rc_file_type.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps' 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+      by (simp add:initp_intact_I_others)  moreover
+    have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+    proof-
+      have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+      proof-
+        have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+          using ev tau SPab af'_cfd'(5) 
+          by (auto simp:obj2sobj.simps cp2sproc.simps ncf_parent etype_of_file_def
+            split:option.splits   intro!:etype_aux_prop3)
+        thus ?thesis using SFab tau ev
+          by (auto simp:obj2sobj.simps split:option.splits if_splits)
+      qed
+      moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+        using ev tau SFab SPab valid ncf_parent
+        by (auto simp:source_dir_simps obj2sobj.simps 
+                split:if_splits option.splits)
+      ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]
+        nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+        by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+    qed
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+      initp_intact_but (s @ s') (SFile (t, sd) None) \<and>
+      obj2sobj (s @ s') obj = SFile (t, sd) None \<and>
+      exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t, sd) None) obj"
+      using tau ev
+      apply (rule_tac x = "e#sb@sa" in exI)
+      by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+  qed 
+next
+  case (ai'_init i t) 
+  hence initi: "i \<in> init_ipcs" using init_ipc_has_type
+    by (simp add:bidirect_in_init_def)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+      and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+      and notboth: "not_both_sproc (SIPC t (Some i)) sobj'"
+      and exso': "exists s' obj'"
+    from nodels' initi have exi: "i \<in> current_ipcs s'" 
+      by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+)    
+    have "obj2sobj s' (IPC i) = SIPC t (Some i)"
+    proof-
+      have "obj2sobj [] (IPC i) = SIPC t (Some i)"  
+        using ai'_init initi by (auto simp:obj2sobj.simps)
+      thus ?thesis using vss' exi nodels' initi
+        by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps)
+    qed
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+             initp_intact_but (s @ s') (SIPC t (Some i)) \<and>
+             obj2sobj (s @ s') obj = SIPC t (Some i) \<and>
+             exists (s @ s') obj \<and> sobj_source_eq_obj (SIPC t (Some i)) obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI)
+      by (simp add:vss' sobjs' nodels' intacts' exi exso' del:obj2sobj.simps)
+  qed
+next
+  case (ai'_cipc r fr pt u srp)
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and Both:"not_both_sproc (SIPC (default_ipc_create_type r) None) sobj'"
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" 
+      and exobj':"exists s' obj'"
+    with ai'_cipc(1) notUkn obtain s p where
+      SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+      expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and
+      soab: "obj2sobj (s@s') obj' = sobj'" and 
+      exsoab: "exists (s@s') obj'" and
+      intactab: "initp_intact (s@s')" and
+      nodelab: "no_del_event (s@s')"
+      apply (drule_tac s'= "s'" and obj' = obj' in all_sobjs_E0, auto) 
+      apply (frule obj2sobj_proc, erule exE)
+      by (auto intro:nodel_exists_remains)
+    obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto
+    
+    have valid: "valid (e # \<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau expab by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ai'_cipc(3) SPab
+        by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+      ultimately show ?thesis using vsab tau
+        by (rule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+        by (case_tac obj', simp+)   moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'" 
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  
+        using soab tau valid notUkn nodel ev exsoab
+        by (auto simp:obj2sobj.simps cp2sproc_simps' 
+             simp del:cp2sproc.simps split:option.splits)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+      by (simp add:initp_intact_I_others)  moreover
+    have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None"
+      using ev tau SPab nodel 
+        nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>]
+      by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps 
+              split:option.splits  dest:no_del_event_cons_D)
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+      initp_intact_but (s @ s') (SIPC (default_ipc_create_type r) None) \<and>
+      obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and>
+      exists (s @ s') obj \<and> sobj_source_eq_obj (SIPC (default_ipc_create_type r) None) obj"
+      using tau ev
+      by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, auto)
+  qed 
+next
+  case (ap'_init p r fr t u)
+  hence initp: "p \<in> init_processes" using init_proc_has_role
+    by (simp add:bidirect_in_init_def)
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'"
+      and Nodels': "no_del_event s'"and Intacts':"initp_intact s'"
+      and notboth: "not_both_sproc (SProc (r,fr,t,u) (Some p)) sobj'"
+      and exso': "exists s' obj'"
+    from Nodels' initp have exp: "p \<in> current_procs s'" 
+      apply (drule_tac obj = "Proc p" in nodel_imp_un_deleted)
+      by (drule not_deleted_imp_exists, simp+)
+    with Intacts' initp ap'_init 
+    have "obj2sobj s' (Proc p) = SProc (r, fr, t, u) (Some p)"
+      by (auto simp:initp_intact_def split:option.splits)
+    thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+             exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> 
+             initp_intact_but (s @ s') (SProc (r, fr, t, u) (Some p)) \<and>
+             obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and>
+             exists (s @ s') obj \<and> 
+             sobj_source_eq_obj (SProc (r, fr, t, u) (Some p)) obj"
+      apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p" in exI)
+      by (simp add:VSs' SOs' Nodels' Intacts' initp intact_imp_butp exp exso' 
+               del:obj2sobj.simps)
+  qed
+next
+  case (ap'_crole r fr t u srp r')
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and Both:"not_both_sproc (SProc (r', fr, t, u) srp) sobj'"
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_crole(1,2) obtain s p where
+      VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+      and nodelab: "no_del_event (s@s')"
+      and butab: "initp_intact_but (s@s') (SProc (r, fr, t, u) srp)"
+      and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+      and exp:"exists (s@s') (Proc p)" and exobj':"exists (s@s') obj'"
+      and sreq: "sobj_source_eq_obj (SProc (r, fr, t, u) srp) (Proc p)"
+      by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains)
+    from VSab SPab sreq exp have srpeq: "srp = Some p" 
+      by (simp add:proc_source_eq_prop)
+    with exp VSab SPab have initp: "p \<in> init_processes"
+      by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits) 
+    obtain e \<tau> where ev: "e = ChangeRole p r'" 
+      and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_crole(3) SPab 
+        by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact_but (e#\<tau>) (SProc (r', fr, t, u) srp)"
+      using butab tau ev valid initp srpeq nodel
+      by (simp add:initp_intact_butp_I_crole)  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau
+      by (case_tac obj', simp+)  moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by (auto)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by auto
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False"
+        using Both SOab' notUkn 
+        by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc p) = SProc (r', fr, t, u) srp"
+      using SPab tau vs_tau ev valid
+      by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+              split:option.splits)  moreover
+    have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp   moreover 
+    have "sobj_source_eq_obj (SProc (r', fr, t, u) srp) (Proc p)"
+      using sreq by (case_tac srp, simp+)
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> 
+      initp_intact_but (s @ s') (SProc (r', fr, t, u) srp) \<and> 
+      obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and>
+      exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (r', fr, t, u) srp) obj"
+      using ev tau
+      apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+      by (rule_tac x = "Proc p" in exI, auto)
+  qed
+next
+  case (ap'_chown r fr t u srp u' nr)
+  show ?case 
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and Both:"not_both_sproc (SProc (nr,fr,chown_type_aux r nr t,u') srp) sobj'"
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_chown(1,2) obtain s p where
+      VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+      and nodelab: "no_del_event (s@s')"
+      and butab: "initp_intact_but (s@s') (SProc (r, fr, t, u) srp)"
+      and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+      and exp:"exists (s@s') (Proc p)" and exobj':"exists (s@s') obj'"
+      and sreq: "sobj_source_eq_obj (SProc (r, fr, t, u) srp) (Proc p)"
+      by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains)
+    from VSab SPab sreq exp have srpeq: "srp = Some p" 
+      by (simp add:proc_source_eq_prop)
+    with exp VSab SPab have initp: "p \<in> init_processes"
+      by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits) 
+    obtain e \<tau> where ev: "e = ChangeOwner p u'" 
+      and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp ap'_chown(3) by (simp)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_chown(5) SPab 
+        by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+                split:option.splits t_rc_proc_type.splits)
+          (* here is another place of no_limit of clone event assumption *)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact_but (e#\<tau>) (SProc (nr,fr,chown_type_aux r nr t,u') srp)"
+      using butab tau ev valid initp srpeq nodel
+      by (simp add:initp_intact_butp_I_chown)  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau
+      by (case_tac obj', simp+)  moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by (auto)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+        by auto
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False"
+        using Both SOab' notUkn 
+        by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc p) = SProc (nr,fr,chown_type_aux r nr t,u') srp"
+      using SPab tau vs_tau ev valid ap'_chown(4)
+      by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+              split:option.splits)  moreover
+    have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp   moreover 
+    have "sobj_source_eq_obj (SProc (nr,fr,chown_type_aux r nr t,u') srp) (Proc p)"
+      using sreq by (case_tac srp, simp+)
+    ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> 
+      initp_intact_but (s @ s') (SProc (nr,fr,chown_type_aux r nr t,u') srp) \<and> 
+      obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and>
+      exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (nr,fr,chown_type_aux r nr t,u') srp) obj"
+      using ev tau
+      apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+      by (rule_tac x = "Proc p" in exI, auto)
+  qed
+next
+  case (ap'_exec r fr pt u sp t sd sf r' fr')
+  show ?case
+  proof (rule allI|rule impI|erule conjE)+
+    fix s' obj' sobj'
+    assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 
+      and Both:"not_both_sproc (SProc (r', fr', exec_type_aux r pt, u) sp) sobj'"
+      and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+    with ap'_exec(3,4) obtain sa f where
+      SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and
+      Exfa: "exists (sa @ s') (File f)" and 
+      buta: "initp_intact (sa @ s')" and
+      othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> exists (sa @s') obj' \<and>
+      no_del_event (sa @ s') \<and> sobj_source_eq_obj (SFile (t, sd) sf) (File f)" 
+      apply (simp only:not_both_sproc.simps)
+      apply (erule_tac x = s' in allE, erule_tac x = obj' in allE)
+      apply (erule_tac x = sobj' in allE, auto)
+      by (frule obj2sobj_file, auto intro:nodel_exists_remains)
+    with SFa Exfa othersa ap'_exec(1,2) Both notUkn obtain sb p where
+      VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'"
+      and nodelab: "no_del_event (sb@sa@s')"
+      and butab: "initp_intact_but (sb@sa@s') (SProc (r, fr, pt, u) sp)"
+      and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp"
+      and exp:"exists (sb@sa@s') (Proc p)" and exobj':"exists (sb@sa@s') obj'"
+      and sreq: "sobj_source_eq_obj (SProc (r, fr, pt, u) sp) (Proc p)"
+      by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains)
+    from VSab SPab sreq exp have srpeq: "sp = Some p" by (simp add:proc_source_eq_prop)
+    with exp VSab SPab have initp: "p \<in> init_processes"
+      by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits) 
+    obtain e \<tau> where ev: "e = Execute p f" 
+      and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto
+    hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+    from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')" 
+      apply (drule_tac obj = "File f" in nodel_imp_un_deleted)
+      by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+    from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf"
+      by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all)
+
+    have valid: "valid (e#\<tau>)" 
+    proof-
+      have "os_grant \<tau> e"
+        using ev tau exp by (simp add:exf)
+      moreover have "rc_grant \<tau> e" 
+        using ev tau ap'_exec(5) SPab SFab
+        by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+                split:if_splits option.splits)
+      ultimately show ?thesis using vs_tau
+        by (erule_tac vs_step, simp+)
+    qed  moreover
+    have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover
+    have "initp_intact_but (e#\<tau>) (SProc (r', fr', exec_type_aux r pt, u) sp)"
+      using butab tau ev valid initp srpeq nodel
+      by (simp add:initp_intact_butp_I_exec)  moreover
+    have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau
+      by (case_tac obj', simp+) moreover
+    have "obj2sobj (e#\<tau>) obj' = sobj'"
+    proof-
+      have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+        by (auto simp del:obj2sobj.simps)
+      moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 
+        using SOab' tau ev valid notUkn nodel exobj'
+        obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+        by (auto simp del:obj2sobj.simps)
+      moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False"
+        using Both SOab' notUkn 
+        by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto)
+      ultimately show ?thesis by (case_tac obj', auto)
+    qed  moreover 
+    have "obj2sobj (e#\<tau>) (Proc p) = SProc (r',fr',exec_type_aux r pt, u) sp"
+    proof-
+      have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau
+        by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+      moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau 
+        by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+      ultimately show ?thesis using valid ev ap'_exec(6,7) 
+        by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+    qed  moreover
+    have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp   moreover 
+    have "sobj_source_eq_obj (SProc (r',fr',exec_type_aux r pt,u) sp) (Proc p)"
+      using sreq by (case_tac sp, simp+)
+    ultimately 
+    show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+      exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> 
+      initp_intact_but (s @ s') (SProc (r', fr', exec_type_aux r pt, u) sp) \<and> 
+      obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and>
+      exists (s @ s') obj \<and>
+      sobj_source_eq_obj (SProc (r', fr', exec_type_aux r pt, u) sp) obj"
+      using ev tau
+      apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI)
+      by (rule_tac x = "Proc p" in exI, auto)
+  qed
+qed
+
+lemma all_sobjs_E2: 
+  "\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown; 
+    not_both_sproc sobj sobj'; no_del_event s'; initp_intact s'\<rbrakk>
+   \<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and>
+                no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj \<and> 
+                obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj \<and> 
+                sobj_source_eq_obj sobj obj"
+by (drule all_sobjs_E2_aux, auto)
+
+end
+
+end
\ No newline at end of file