theory CNodeInv_AI

lemma cap_swap_cap_refs_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace>
    cap_swap c a c' b \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (simp add:cap_swap_def) apply wp apply (simp add: cap_refs_respects_device_region_def) apply (rule hoare_strengthen_post[OF CSpace_AI.set_cdt_cap_refs_respects_device_region]) apply simp apply wp+ apply (clarsimp simp add: cap_refs_respects_device_region_def cte_wp_at_caps_of_state
                              cap_range_respects_device_region_def
                    simp del: split_paired_All split_paired_Ex
           | (wp hoare_vcg_all_lift hoare_vcg_imp_lift)+)+ apply (frule_tac x = a in spec) apply (frule_tac x = b in spec) apply (clarsimp simp: weak_derived_cap_range) apply (intro conjI impI allI) apply (simp add: weak_derived_cap_range weak_derived_cap_is_device)+ apply (rule ccontr) apply simp apply (rule disjI2) apply (intro conjI impI) apply (simp add: weak_derived_cap_range weak_derived_cap_is_device)+ apply (rule ccontr) apply simp apply (simp add: weak_derived_cap_range weak_derived_cap_is_device)+ apply (rule ccontr) apply simp apply (rule disjI2) apply (rule ccontr) apply (clarsimp simp add: weak_derived_cap_range weak_derived_cap_is_device)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>y ya slot1_p slot2_p cdt yb s f. cap_refs_respects_device_region (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(a := is_original_cap (trans_state f s) b), is_original_cap := (is_original_cap (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(a := is_original_cap (trans_state f s) b)\<rparr>))(b := is_original_cap (trans_state f s) a)\<rparr>) = cap_refs_respects_device_region (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b)\<rparr>))(b := is_original_cap s a)\<rparr>)
 2. \<And>y ya slot1_p slot2_p cdt. \<lbrace>?B5 y ya slot1_p slot2_p cdt\<rbrace> set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a)) \<lbrace>\<lambda>yb s. cap_refs_respects_device_region (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b)\<rparr>))(b := is_original_cap s a)\<rparr>)\<rbrace>
 3. \<And>y ya slot1_p slot2_p. \<lbrace>?B4 y ya slot1_p slot2_p\<rbrace> gets cdt \<lbrace>?B5 y ya slot1_p slot2_p\<rbrace>
 4. \<And>y ya slot1_p. \<lbrace>?B3 y ya slot1_p\<rbrace> gets (\<lambda>s. cdt s b) \<lbrace>?B4 y ya slot1_p\<rbrace>
 5. \<And>y ya. \<lbrace>?B2 y ya\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B3 y ya\<rbrace>
 6. \<And>y. \<lbrace>?B1 y\<rbrace> set_cap c b \<lbrace>?B2 y\<rbrace>
 7. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 8. \<And>s. (cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>y ya slot1_p slot2_p cdt. \<lbrace>?B5 y ya slot1_p slot2_p cdt\<rbrace> set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a)) \<lbrace>\<lambda>yb s. cap_refs_respects_device_region (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b)\<rparr>))(b := is_original_cap s a)\<rparr>)\<rbrace>
 2. \<And>y ya slot1_p slot2_p. \<lbrace>?B4 y ya slot1_p slot2_p\<rbrace> gets cdt \<lbrace>?B5 y ya slot1_p slot2_p\<rbrace>
 3. \<And>y ya slot1_p. \<lbrace>?B3 y ya slot1_p\<rbrace> gets (\<lambda>s. cdt s b) \<lbrace>?B4 y ya slot1_p\<rbrace>
 4. \<And>y ya. \<lbrace>?B2 y ya\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B3 y ya\<rbrace>
 5. \<And>y. \<lbrace>?B1 y\<rbrace> set_cap c b \<lbrace>?B2 y\<rbrace>
 6. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 7. \<And>s. (cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>y ya slot1_p slot2_p cdt rv s. cap_refs_respects_device_region s \<Longrightarrow> cap_refs_respects_device_region (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(a := is_original_cap s b)\<rparr>))(b := is_original_cap s a)\<rparr>)
 2. \<And>y ya slot1_p slot2_p. \<lbrace>?B4 y ya slot1_p slot2_p\<rbrace> gets cdt \<lbrace>\<lambda>cdt. cap_refs_respects_device_region\<rbrace>
 3. \<And>y ya slot1_p. \<lbrace>?B3 y ya slot1_p\<rbrace> gets (\<lambda>s. cdt s b) \<lbrace>?B4 y ya slot1_p\<rbrace>
 4. \<And>y ya. \<lbrace>?B2 y ya\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B3 y ya\<rbrace>
 5. \<And>y. \<lbrace>?B1 y\<rbrace> set_cap c b \<lbrace>?B2 y\<rbrace>
 6. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 7. \<And>s. (cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>y ya slot1_p slot2_p. \<lbrace>?B4 y ya slot1_p slot2_p\<rbrace> gets cdt \<lbrace>\<lambda>cdt. cap_refs_respects_device_region\<rbrace>
 2. \<And>y ya slot1_p. \<lbrace>?B3 y ya slot1_p\<rbrace> gets (\<lambda>s. cdt s b) \<lbrace>?B4 y ya slot1_p\<rbrace>
 3. \<And>y ya. \<lbrace>?B2 y ya\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B3 y ya\<rbrace>
 4. \<And>y. \<lbrace>?B1 y\<rbrace> set_cap c b \<lbrace>?B2 y\<rbrace>
 5. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 6. \<And>s. (cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B1 y\<rbrace> set_cap c b \<lbrace>\<lambda>ya. cap_refs_respects_device_region\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 3. \<And>s. (cap_refs_respects_device_region and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa. \<lbrakk>\<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa\<rbrakk> \<Longrightarrow> ((aa, ba) = a \<longrightarrow> (\<forall>x. (a = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))))) \<and> ((aa, ba) \<noteq> a \<longrightarrow> (\<forall>x. ((aa, ba) = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (caps_of_state s (aa, ba) = Some x \<longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa. \<lbrakk>\<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; \<forall>cap. caps_of_state s a = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)))\<rbrakk> \<Longrightarrow> ((aa, ba) = a \<longrightarrow> (\<forall>x. (a = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))))) \<and> ((aa, ba) \<noteq> a \<longrightarrow> (\<forall>x. ((aa, ba) = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (caps_of_state s (aa, ba) = Some x \<longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa. \<lbrakk>\<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; \<forall>cap. caps_of_state s a = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); \<forall>cap. caps_of_state s b = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)))\<rbrakk> \<Longrightarrow> ((aa, ba) = a \<longrightarrow> (\<forall>x. (a = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))))) \<and> ((aa, ba) \<noteq> a \<longrightarrow> (\<forall>x. ((aa, ba) = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (caps_of_state s (aa, ba) = Some x \<longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> ((aa, ba) = a \<longrightarrow> (\<forall>x. (a = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))))) \<and> ((aa, ba) \<noteq> a \<longrightarrow> (\<forall>x. ((aa, ba) = b \<longrightarrow> (cap_is_device x \<longrightarrow> c = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))) \<and> (caps_of_state s (aa, ba) = Some x \<longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))))) proof (prove)
goal (6 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a; a = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a; a = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a\<rbrakk> \<Longrightarrow> a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 5. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 6. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (5 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); capa = cap; weak_derived x cap; caps_of_state s b = Some cap; weak_derived c' cap; if cap_is_device x then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device x then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = b; a = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range cap \<subseteq> - dom (device_state (machine_state s))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a\<rbrakk> \<Longrightarrow> a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 5. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (5 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); capa = cap; weak_derived x cap; caps_of_state s b = Some cap; weak_derived c' cap; if cap_is_device x then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device x then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = b; a = b; c = x; \<not> (cap_is_device x \<or> cap_range cap \<subseteq> - dom (device_state (machine_state s)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a\<rbrakk> \<Longrightarrow> a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 5. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (4 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a\<rbrakk> \<Longrightarrow> a = b \<or> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (4 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a\<rbrakk> \<Longrightarrow> (cap_is_device x \<longrightarrow> c' = x \<longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))) \<and> (c' = x \<longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (5 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a; cap_is_device x; c' = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a; c' = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 5. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (4 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived x capa; if cap_is_device c then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device x then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a; c' = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range capa \<subseteq> - dom (device_state (machine_state s))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (4 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived x capa; if cap_is_device c then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device x then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) = a; c' = x; \<not> (cap_is_device x \<or> cap_range capa \<subseteq> - dom (device_state (machine_state s)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 4. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (3 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; cap_is_device x; c = x\<rbrakk> \<Longrightarrow> cap_range x \<subseteq> dom (device_state (machine_state s))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s))
 3. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived x cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device x then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device c' then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); b \<noteq> a; (aa, ba) = b; c = x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range cap \<subseteq> - dom (device_state (machine_state s))
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived x cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device x then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device c' then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); b \<noteq> a; (aa, ba) = b; c = x; \<not> (cap_is_device x \<or> cap_range cap \<subseteq> - dom (device_state (machine_state s)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> (aa, ba) = b \<or> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x\<rbrakk> \<Longrightarrow> cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa x. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device capa then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x; \<not> (cap_is_device x \<or> cap_range x \<subseteq> - dom (device_state (machine_state s)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba cap capa x xa y. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s))); caps_of_state s a = Some cap; weak_derived c cap; caps_of_state s b = Some capa; weak_derived c' capa; if cap_is_device c then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); if cap_is_device c' then cap_range capa \<subseteq> dom (device_state (machine_state s)) else cap_range capa \<subseteq> - dom (device_state (machine_state s)); (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some x; \<not> cap_is_device x; xa \<in> cap_range x; device_state (machine_state s) xa = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!