theory CSpaceInv_AI

lemma rab_inv[wp]:
  "\<lbrace>P\<rbrace> resolve_address_bits slot \<lbrace>\<lambda>rv. P\<rbrace>" unfolding resolve_address_bits_def proof (induct slot rule: resolve_address_bits'.induct) case (1 z cap cref) show ?case apply (clarsimp simp add: valid_def) apply (subst (asm) resolve_address_bits'.simps) apply (cases cap) apply (auto simp: in_monad)[5] defer apply (auto simp: in_monad)[6] apply (rename_tac obj_ref nat list) apply (simp only: cap.simps) apply (case_tac "nat + length list = 0") apply (simp add: fail_def) apply (simp only: if_False) apply (case_tac a) apply (simp only: K_bind_def) apply (drule in_bindE_L, elim disjE conjE exE)+ apply (simp only: split: if_split_asm) apply (simp add: returnOk_def return_def) apply (drule in_bindE_L, elim disjE conjE exE)+ apply (simp only: split: if_split_asm) prefer 2 apply (clarsimp simp: in_monad) apply (drule (8) 1) apply (clarsimp simp: in_monad) apply (drule in_inv_by_hoareD [OF get_cap_inv]) apply (auto simp: in_monad valid_def)[1] apply (clarsimp simp: in_monad) apply (clarsimp simp: in_monad) apply (clarsimp simp: in_monad) apply (clarsimp simp: in_monad) apply (clarsimp simp: in_monad) apply (simp only: K_bind_def in_bindE_R) apply (elim conjE exE) apply (simp only: split: if_split_asm) apply (simp add: in_monad split: if_split_asm) apply (simp only: K_bind_def in_bindE_R) apply (elim conjE exE) apply (simp only: split: if_split_asm) prefer 2 apply (clarsimp simp: in_monad) apply (drule in_inv_by_hoareD [OF get_cap_inv]) apply simp apply (drule (8) "1") apply (clarsimp simp: in_monad valid_def) apply (drule in_inv_by_hoareD [OF get_cap_inv]) apply (auto simp: in_monad) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> resolve_address_bits slot \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> resolve_address_bits' TYPE('a) slot \<lbrace>\<lambda>rv. P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>z cap cref. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc. \<lbrakk>cap = CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63)) s'); (Inr rva, sta) \<in> fst ((returnOk $ take x62 (drop (length x63) cref)) st); (Inr rvb, stb) \<in> fst ((returnOk $ drop (x62 + length x63) cref) sta); rvb \<noteq> []; (Inr rvc, stc) \<in> fst ((liftE $ get_cap (x61, rva)) stb); is_cnode_cap rvc\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. P\<rbrace> proof (state)
this:
\<lbrakk>cap = CNodeCap ?x61.0 ?x62.0 ?x63.0; ?x62.0 + length ?x63.0 \<noteq> 0; (Inr ?v, ?s') \<in> fst (whenE (\<not> ?x63.0 \<le> cref) (throwError $ GuardMismatch (length cref) ?x63.0) ?s); (Inr ?rv, ?st) \<in> fst (whenE (length cref < ?x62.0 + length ?x63.0) (throwError $ DepthMismatch (length cref) (?x62.0 + length ?x63.0)) ?s'); (Inr ?rva, ?sta) \<in> fst ((returnOk $ take ?x62.0 (drop (length ?x63.0) cref)) ?st); (Inr ?rvb, ?stb) \<in> fst ((returnOk $ drop (?x62.0 + length ?x63.0) cref) ?sta); ?rvb \<noteq> []; (Inr ?rvc, ?stc) \<in> fst ((liftE $ get_cap (?x61.0, ?rva)) ?stb); is_cnode_cap ?rvc\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> resolve_address_bits' z (?rvc, ?rvb) \<lbrace>\<lambda>rv. P\<rbrace>

goal (1 subgoal):
 1. \<And>z cap cref. (\<And>x61 x62 x63 v s s' rv st rva sta rvb stb rvc stc. \<lbrakk>cap = CNodeCap x61 x62 x63; x62 + length x63 \<noteq> 0; (Inr v, s') \<in> fst (whenE (\<not> x63 \<le> cref) (throwError $ GuardMismatch (length cref) x63) s); (Inr rv, st) \<in> fst (whenE (length cref < x62 + length x63) (throwError $ DepthMismatch (length cref) (x62 + length x63)) s'); (Inr rva, sta) \<in> fst ((returnOk $ take x62 (drop (length x63) cref)) st); (Inr rvb, stb) \<in> fst ((returnOk $ drop (x62 + length x63) cref) sta); rvb \<noteq> []; (Inr rvc, stc) \<in> fst ((liftE $ get_cap (x61, rva)) stb); is_cnode_cap rvc\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> resolve_address_bits' z (rvc, rvb) \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (resolve_address_bits' z (cap, cref) s)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (12 subgoals):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = NullCap\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b x21 x22 x23 x24. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b x31 x32 x33. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b x41 x42 x43. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b x51 x52 x53. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b x61 x62 x63. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b x7. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> P b
 8. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = DomainCap\<rbrakk> \<Longrightarrow> P b
 9. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = IRQControlCap\<rbrakk> \<Longrightarrow> P b
 10. \<And>s a b x10. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> P b
A total of 12 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>s a b x61 x62 x63. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b x7. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = DomainCap\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = IRQControlCap\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b x10. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b x111 x112 x113. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b x12. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (7 subgoals):
 1. \<And>s a b x7. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = DomainCap\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = IRQControlCap\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b x10. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b x111 x112 x113. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b x12. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b x61 x62 x63. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x61 x62 x63. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list. \<lbrakk>P s; (a, b) \<in> fst ((case cap of CNodeCap oref radix_bits guard \<Rightarrow> if radix_bits + length guard = 0 then fail else doE whenE (\<not> guard \<le> cref) (throwError $ GuardMismatch (length cref) guard);
whenE (length cref < radix_bits + length guard) (throwError $ DepthMismatch (length cref) (radix_bits + length guard));
offset <- returnOk $ take radix_bits (drop (length guard) cref);
rest <- returnOk $ drop (radix_bits + length guard) cref;
if rest = [] then returnOk ((oref, offset), []) else doE next_cap <- liftE $ get_cap (oref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((oref, offset), rest)
odE
odE | _ \<Rightarrow> throwError InvalidRoot) s); cap = CNodeCap obj_ref nat list\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list. \<lbrakk>P s; (a, b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s a b obj_ref nat list. \<lbrakk>P s; (a, b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list = 0\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list. \<lbrakk>P s; (a, b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list. \<lbrakk>P s; (a, b) \<in> fst ((if nat + length list = 0 then fail else doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; (Inl aa, b) \<in> fst ((doE y <- whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
y <- whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (6 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); (Inl aa, b) \<in> fst ((if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (7 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr [], s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest = []; (Inl aa, b) \<in> fst (returnOk ((obj_ref, offset), []) s''c)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (6 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (7 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); (Inl aa, b) \<in> fst ((if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)) s''d)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (8 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inl aa, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inl aa, b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 8. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (8 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inl aa, b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inl aa, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 8. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (7 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inl aa, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (7 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inl aa, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d); \<lbrace>P\<rbrace> resolve_address_bits' z (next_cap, rest) \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (7 subgoals):
 1. \<And>s b obj_ref nat list aa s''d next_cap. \<lbrakk>P s; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s''d) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inl aa, b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s''d); \<lbrace>P\<rbrace> resolve_address_bits' z (next_cap, drop (nat + length list) cref) \<lbrace>\<lambda>rv. P\<rbrace>; list \<le> cref\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (7 subgoals):
 1. \<And>s b obj_ref nat list aa s''d next_cap. \<lbrakk>P s; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; is_cnode_cap next_cap; (Inl aa, b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s''d); \<lbrace>P\<rbrace> resolve_address_bits' z (next_cap, drop (nat + length list) cref) \<lbrace>\<lambda>rv. P\<rbrace>; list \<le> cref; s''d = s\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 7. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (6 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inl aa, b) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 6. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (5 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya s''b offset. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inl aa, b) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 5. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (4 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y s''a ya. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inl aa, b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 4. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (3 subgoals):
 1. \<And>s a b obj_ref nat list aa s'' y. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inl aa, b) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'')\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 3. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s a b obj_ref nat list aa. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inl aa; (Inl aa, b) \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; (a, b) \<in> fst ((doE whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list);
whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list));
offset <- returnOk $ take nat (drop (length list) cref);
rest <- returnOk $ drop (nat + length list) cref;
if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE
odE) s); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba. \<lbrakk>P s; \<exists>s'' y. (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s) \<and> (\<exists>s''a y. (Inr y, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s'') \<and> (\<exists>s'' offset. (Inr offset, s'') \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a) \<and> (\<exists>s''a rest. (Inr rest, s''a) \<in> fst ((returnOk $ drop (nat + length list) cref) s'') \<and> (Inr ba, b) \<in> fst ((if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''a)))); cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); (Inr ba, b) \<in> fst ((if rest = [] then returnOk ((obj_ref, offset), []) else doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr [], s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest = []; (Inr ba, b) \<in> fst (returnOk ((obj_ref, offset), []) s''c)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr ba, b) \<in> fst ((doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr ba, b) \<in> fst ((doE next_cap <- liftE $ get_cap (obj_ref, offset);
if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)
odE) s''c)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; \<exists>s'' next_cap. (Inr next_cap, s'') \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c) \<and> (Inr ba, b) \<in> fst ((if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)) s'')\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); (Inr ba, b) \<in> fst ((if is_cnode_cap next_cap then resolve_address_bits' z (next_cap, rest) else returnOk ((obj_ref, offset), rest)) s''d)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ba, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ba, b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); \<not> is_cnode_cap next_cap; (Inr ba, b) \<in> fst (returnOk ((obj_ref, offset), rest) s''d)\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ba, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s b obj_ref nat list next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, b) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); \<not> is_cnode_cap next_cap; list \<le> cref\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ba, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (2 subgoals):
 1. \<And>s b obj_ref nat list next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; \<not> is_cnode_cap next_cap; list \<le> cref; b = s\<rbrakk> \<Longrightarrow> P b
 2. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ba, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; cap = CNodeCap obj_ref nat list; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ba, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b obj_ref nat list ba s'' y s''a ya s''b offset s''c rest s''d next_cap. \<lbrakk>P s; nat + length list \<noteq> 0; a = Inr ba; (Inr y, s'') \<in> fst (whenE (\<not> list \<le> cref) (throwError $ GuardMismatch (length cref) list) s); (Inr ya, s''a) \<in> fst (whenE (length cref < nat + length list) (throwError $ DepthMismatch (length cref) (nat + length list)) s''); (Inr offset, s''b) \<in> fst ((returnOk $ take nat (drop (length list) cref)) s''a); (Inr rest, s''c) \<in> fst ((returnOk $ drop (nat + length list) cref) s''b); rest \<noteq> []; (Inr next_cap, s''d) \<in> fst ((liftE $ get_cap (obj_ref, offset)) s''c); is_cnode_cap next_cap; (Inr ba, b) \<in> fst (resolve_address_bits' z (next_cap, rest) s''d); \<lbrace>P\<rbrace> resolve_address_bits' z (next_cap, rest) \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s b obj_ref nat list aa ba bb s''d next_cap. \<lbrakk>P s; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; (next_cap, s''d) \<in> fst (get_cap (obj_ref, take nat (drop (length list) cref)) s); is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s''d); \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, x) \<Rightarrow> P x); list \<le> cref\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s b obj_ref nat list aa ba bb s''d next_cap. \<lbrakk>P s; 0 < nat \<or> list \<noteq> []; \<not> length cref \<le> nat + length list; is_cnode_cap next_cap; (Inr ((aa, ba), bb), b) \<in> fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s''d); \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (resolve_address_bits' z (next_cap, drop (nat + length list) cref) s). case x of (r, x) \<Rightarrow> P x); list \<le> cref; s''d = s\<rbrakk> \<Longrightarrow> P b proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P\<rbrace> resolve_address_bits' z (cap, cref) \<lbrace>\<lambda>rv. P\<rbrace>

goal:
No subgoals!