theory Delete_C

lemma cap_zombie_cap_set_capZombieNumber_spec:
  "\<forall>cap s. \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap
                     \<and> unat (n_' s) \<le> zombieCTEs (capZombieType cap)\<rbrace>
     Call cap_zombie_cap_set_capZombieNumber_'proc
   {s'. ccap_relation (capZombieNumber_update (\<lambda>_. unat (n_' s)) cap)
               (ret__struct_cap_C_' s')}" apply vcg apply (rule context_conjI, simp add: cap_get_tag_isCap) apply clarsimp apply (frule(2) ccap_zombie_radix_less3) apply (rule conjI, unat_arith) apply clarsimp apply (frule(2) ccap_zombie_radix_less1) apply (clarsimp simp: cap_zombie_cap_lift
                        ccap_relation_def map_option_Some_eq2
                        cap_to_H_def get_capZombieBits_CL_def
                 split: if_split_asm) apply (simp add: mask_def word_bw_assocs word_ao_dist) apply (rule sym, rule less_mask_eq[where n=5, unfolded mask_def, simplified]) apply unat_arith apply (clarsimp simp: Let_def mask_2pm1[symmetric]) apply (subst unat_Suc2, clarsimp)+ apply (subst less_mask_eq, erule order_less_le_trans, simp)+ apply (simp add: word_ao_dist word_bw_assocs) apply (rule sym, rule less_mask_eq) apply (simp only: word_less_nat_alt) apply (subst unat_power_lower) apply (simp add: word_bits_conv) apply (erule order_le_less_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 \<and> unat \<^bsup>s\<^esup>n \<le> zombieCTEs (capZombieType cap)\<rbrace> Call cap_zombie_cap_set_capZombieNumber_'proc \<lbrace>ccap_relation (capZombieNumber_update (\<lambda>_. unat \<^bsup>s\<^esup>n) cap) \<acute>ret__struct_cap_C\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap capa n. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; unat n \<le> zombieCTEs (capZombieType 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> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := UCAST(32 \<rightarrow> 32) (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) || n && (1 << unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + SCAST(32 signed \<rightarrow> 32) 1)) - 1) && mask 32\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap) ret__struct_cap_C))) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa n. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; unat n \<le> zombieCTEs (capZombieType cap); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> \<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> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := UCAST(32 \<rightarrow> 32) (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) || n && (1 << unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + SCAST(32 signed \<rightarrow> 32) 1)) - 1) && mask 32\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap) ret__struct_cap_C)) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa n. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; unat n \<le> zombieCTEs (capZombieType 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> (\<forall>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1) || n && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap) ret__struct_cap_C) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa n. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; unat n \<le> zombieCTEs (capZombieType cap); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1 < 0x20 \<and> (\<forall>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1) || n && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap) ret__struct_cap_C) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa n. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; unat n \<le> zombieCTEs (capZombieType cap); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C\<rbrakk> \<Longrightarrow> \<forall>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1) || n && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap) ret__struct_cap_C proof (prove)
goal (1 subgoal):
 1. \<And>cap capa n ret__struct_cap_C. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; unat n \<le> zombieCTEs (capZombieType cap); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1) || n && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1\<rparr>; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap) ret__struct_cap_C proof (prove)
goal (1 subgoal):
 1. \<And>cap capa n ret__struct_cap_C. \<lbrakk>ccap_relation cap capa; isZombie cap; capAligned cap; unat n \<le> zombieCTEs (capZombieType cap); cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; get_capZombieBits_CL (cap_zombie_cap_lift capa) < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1) || n && 2 ^ unat (get_capZombieBits_CL (cap_zombie_cap_lift capa) + 1) - 1\<rparr>; cap_get_tag ret__struct_cap_C = 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> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap) ret__struct_cap_C proof (prove)
goal (2 subgoals):
 1. \<And>capa n ret__struct_cap_C. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && mask 5))); unat n \<le> 5; cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F\<rparr>)); isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask 5 = (capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F) && ~~ mask 5 \<and> n = (capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F) && mask 5
 2. \<And>capa n ret__struct_cap_C. \<lbrakk>isZombie (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 (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)))); unat n \<le> zombieCTEs (capZombieType (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_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieNumber_update (\<lambda>_. unat n) (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)))) = (let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && mask (Suc radix)))) proof (prove)
goal (2 subgoals):
 1. \<And>capa n ret__struct_cap_C. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && 0x1F))); unat n \<le> 5; cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F\<rparr>)); isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> n = n && 0x1F
 2. \<And>capa n ret__struct_cap_C. \<lbrakk>isZombie (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 (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)))); unat n \<le> zombieCTEs (capZombieType (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_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieNumber_update (\<lambda>_. unat n) (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)))) = (let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && mask (Suc radix)))) proof (prove)
goal (2 subgoals):
 1. \<And>capa n ret__struct_cap_C. \<lbrakk>capAligned (capability.Zombie (capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift capa) && 0x1F))); unat n \<le> 5; cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && 0xFFFFFFE0 || n && 0x1F\<rparr>)); isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> n < 0x20
 2. \<And>capa n ret__struct_cap_C. \<lbrakk>isZombie (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 (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)))); unat n \<le> zombieCTEs (capZombieType (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_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieNumber_update (\<lambda>_. unat n) (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)))) = (let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && mask (Suc radix)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<lbrakk>isZombie (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 (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)))); unat n \<le> zombieCTEs (capZombieType (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_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> capZombieNumber_update (\<lambda>_. unat n) (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)))) = (let radix = unat (capZombieType_CL (cap_zombie_cap_lift capa)) in capability.Zombie ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && ~~ mask (Suc radix)) (ZombieCNode radix) (unat ((capZombieID_CL (cap_zombie_cap_lift capa) && ~~ (2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) || n && 2 ^ unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1) - 1) && mask (Suc radix)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 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 (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) \<and> n = (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 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) && mask 5))) || n && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5)))) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) \<and> n = (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5))) || n && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5)))) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 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)))) || n && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) \<and> n = (capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) || n && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))))) && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> n = n && mask (Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); capZombieType_CL (cap_zombie_cap_lift capa) && mask 5 < 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); capZombieType_CL (cap_zombie_cap_lift capa) < 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> n < 2 ^ Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) < unat 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); unat (capZombieType_CL (cap_zombie_cap_lift capa)) < unat 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> unat n < unat (2 ^ Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa)))) proof (prove)
goal (2 subgoals):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) < unat 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); unat (capZombieType_CL (cap_zombie_cap_lift capa)) < unat 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))) < LENGTH(32)
 2. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) < unat 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); unat (capZombieType_CL (cap_zombie_cap_lift capa)) < unat 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> unat n < 2 ^ Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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))))))); unat n \<le> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)); cap_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) < unat 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); unat (capZombieType_CL (cap_zombie_cap_lift capa)) < unat 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> unat n < 2 ^ Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))) proof (prove)
goal (1 subgoal):
 1. \<And>capa n ret__struct_cap_C. \<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_lift capa = Some (Cap_zombie_cap (cap_zombie_cap_lift capa)); unat (capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) < unat 0x1C; cap_zombie_cap_lift ret__struct_cap_C = cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>; cap_lift ret__struct_cap_C = Some (Cap_zombie_cap (cap_zombie_cap_lift capa\<lparr>capZombieID_CL := capZombieID_CL (cap_zombie_cap_lift capa) && ~~ mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1)) || n && mask (unat ((capZombieType_CL (cap_zombie_cap_lift capa) && mask 5) + 1))\<rparr>)); unat (capZombieType_CL (cap_zombie_cap_lift capa)) < unat 0x1C; \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift capa))\<rbrakk> \<Longrightarrow> 2 ^ unat (capZombieType_CL (cap_zombie_cap_lift capa)) < 2 ^ Suc (unat (capZombieType_CL (cap_zombie_cap_lift capa))) proof (prove)
goal:
No subgoals!