theory Delete_C

lemma cap_zombie_cap_get_capZombieNumber_spec:
  notes if_cong[cong]
  shows
  "\<forall>cap s. \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap\<rbrace>
     Call cap_zombie_cap_get_capZombieNumber_'proc
   {s'. ret__unsigned_long_' s' = of_nat (capZombieNumber cap)}" apply vcg apply clarsimp apply (rule context_conjI, simp add: cap_get_tag_isCap) apply (frule(2) ccap_zombie_radix_less1) apply (frule(2) ccap_zombie_radix_less3) apply (drule(1) cap_get_tag_to_H) apply clarsimp apply (rule conjI) apply unat_arith apply (fold mask_2pm1) apply (simp add: get_capZombieBits_CL_def Let_def split: if_split_asm) apply (subst unat_Suc2) apply clarsimp apply (subst less_mask_eq, erule order_less_le_trans) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cap s. \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap\<rbrace> Call cap_zombie_cap_get_capZombieNumber_'proc \<lbrace>\<acute>ret__unsigned_long = word_of_nat (capZombieNumber cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap\<rbrakk> \<Longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = get_capZombieBits_CL (cap_zombie_cap_lift capa) \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capZombieID_CL (cap_zombie_cap_lift capa) \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + SCAST(32 signed \<rightarrow> 32) 1 < SCAST(32 signed \<rightarrow> 32) 0x20 \<and> UCAST(32 \<rightarrow> 32) (capZombieID_CL (cap_zombie_cap_lift capa)) && (1 << unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + SCAST(32 signed \<rightarrow> 32) 1)) - 1 = word_of_nat (capZombieNumber cap))) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap\<rbrakk> \<Longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20 \<and> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber cap) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20 \<and> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber cap) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20 \<and> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber cap) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20 \<and> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber cap) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>isZombie cap; capAligned cap; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C; cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (radix + 1))))\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20 \<and> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber cap) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>isZombie (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); capAligned (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20 \<and> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix))))) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>isZombie (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); capAligned (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20
 2. \<And>capa. \<lbrakk>isZombie (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); capAligned (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>isZombie (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); capAligned (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1 = word_of_nat (capZombieNumber (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>isZombie (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); capAligned (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix)))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && mask (unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1)) = word_of_nat (capZombieNumber (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc radix))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) = capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 \<noteq> - 1
 2. \<And>capa. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5))) = capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5))) = capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> 0x1C \<le> 2 ^ 5
 2. \<And>capa. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) (ZombieCNode (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))))); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) = capZombieID_CL (cap_zombie_cap_lift capa) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal:
No subgoals!