theory CNodeInv_R

lemma untyped_inc_n:
  assumes untyped_eq: "isUntypedCap src_cap \<Longrightarrow> scap = src_cap"
                      "isUntypedCap dest_cap \<Longrightarrow> dcap = dest_cap"
  shows "untyped_inc' n" using untyped_inc apply (simp add: n_cap_eq untyped_inc'_def descendants_of'_def parency) apply clarsimp apply (erule_tac x="s_d_swap p src dest" in allE) apply (erule_tac x="s_d_swap p' src dest" in allE) apply (case_tac "p=dest") apply simp apply (case_tac "p'=src", simp) apply (clarsimp simp:untyped_eq) apply (case_tac "p'=dest", simp) apply (clarsimp simp: s_d_swap_def untyped_eq) apply clarsimp apply (case_tac "p=src") apply clarsimp apply (case_tac "p'=dest", simp) apply (clarsimp simp:untyped_eq) apply (case_tac "p'=src", simp) apply (clarsimp simp:untyped_eq) apply clarsimp apply (case_tac "p'=src") apply (clarsimp simp:untyped_eq) apply simp apply (case_tac "p'=dest", clarsimp simp:untyped_eq) apply (clarsimp simp:untyped_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc' n proof (prove)
using this:
untyped_inc' m

goal (1 subgoal):
 1. untyped_inc' n proof (prove)
goal (1 subgoal):
 1. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> p' \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> p' \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> p \<rightarrow> p' \<and> usableUntypedRange c = {} \<or> m \<turnstile> p' \<rightarrow> p \<and> usableUntypedRange c' = {} \<or> p = p')) \<Longrightarrow> \<forall>p p' c. (\<exists>n. (p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)))) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. (p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap) \<and> (p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')))) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> p' \<rightarrow> p \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> p \<rightarrow> p' \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> p \<rightarrow> p' \<and> usableUntypedRange c = {} \<or> m \<turnstile> p' \<rightarrow> p \<and> usableUntypedRange c' = {} \<or> p = p')); p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>p' c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> p' \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> p' \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> p' \<and> usableUntypedRange c = {} \<or> m \<turnstile> p' \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = p'))\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest))\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest)); p = dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')
 2. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest)); p \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' n c' n'. \<lbrakk>m src = Some (CTE src_cap n); isUntypedCap src_cap; p' = dest \<longrightarrow> n = n' \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange src_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> src = s_d_swap p' src dest); p = dest\<rbrakk> \<Longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange scap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange scap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> dest = p')
 2. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest)); p \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (3 subgoals):
 1. \<And>p p' n n'. \<lbrakk>m src = Some (CTE src_cap n); isUntypedCap src_cap; m dest = Some (CTE dest_cap n'); isUntypedCap dest_cap; (untypedRange src_cap \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange dest_cap = {}) \<and> (untypedRange src_cap \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange dest_cap = {}) \<and> (untypedRange dest_cap \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap = untypedRange dest_cap \<longrightarrow> m \<turnstile> src \<rightarrow> dest \<and> usableUntypedRange src_cap = {} \<or> m \<turnstile> dest \<rightarrow> src \<and> usableUntypedRange dest_cap = {}); p = dest; p' = src\<rbrakk> \<Longrightarrow> (untypedRange src_cap \<subset> untypedRange dest_cap \<longrightarrow> untypedRange src_cap \<inter> usableUntypedRange dcap = {}) \<and> (untypedRange dest_cap \<subset> untypedRange src_cap \<longrightarrow> untypedRange dest_cap \<inter> usableUntypedRange scap = {}) \<and> (untypedRange src_cap = untypedRange dest_cap \<longrightarrow> m \<turnstile> src \<rightarrow> dest \<and> usableUntypedRange scap = {} \<or> m \<turnstile> dest \<rightarrow> src \<and> usableUntypedRange dcap = {})
 2. \<And>p p' n c' n'. \<lbrakk>m src = Some (CTE src_cap n); isUntypedCap src_cap; p' = dest \<longrightarrow> n = n' \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange src_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> src = s_d_swap p' src dest); p = dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange scap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange scap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> dest = p')
 3. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest)); p \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' n c' n'. \<lbrakk>m src = Some (CTE src_cap n); isUntypedCap src_cap; p' = dest \<longrightarrow> n = n' \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange src_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> src = s_d_swap p' src dest); p = dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange scap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange scap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> dest = p')
 2. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest)); p \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' n c' n'. \<lbrakk>m src = Some (CTE src_cap n); isUntypedCap src_cap; p' = dest \<longrightarrow> n = n' \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange src_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> src = s_d_swap p' src dest); p = dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange src_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange c' = {}) \<and> (untypedRange src_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange scap = {}) \<and> (untypedRange src_cap = untypedRange c' \<longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange scap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> src \<and> usableUntypedRange c' = {} \<or> dest = p')
 2. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest)); p \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>p = dest \<longrightarrow> m src = Some (CTE src_cap n) \<and> c = scap; p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap) \<and> (p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)); isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> s_d_swap p src dest = s_d_swap p' src dest)); p \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n)\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n); p = src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')
 2. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p' n c' n'. \<lbrakk>isUntypedCap dest_cap; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> n = n' \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dest_cap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dest_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p'); m dest = Some (CTE dest_cap n)\<rbrakk> \<Longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dcap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dcap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p')
 2. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (3 subgoals):
 1. \<And>p' n n'. \<lbrakk>isUntypedCap dest_cap; m src = Some (CTE src_cap n'); isUntypedCap src_cap; (untypedRange dest_cap \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange src_cap = {}) \<and> (untypedRange dest_cap \<subset> untypedRange src_cap \<longrightarrow> m \<turnstile> src \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> src \<and> untypedRange src_cap \<inter> usableUntypedRange dest_cap = {}) \<and> (untypedRange dest_cap = untypedRange src_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> src \<and> usableUntypedRange dest_cap = {} \<or> m \<turnstile> src \<rightarrow> dest \<and> usableUntypedRange src_cap = {}); m dest = Some (CTE dest_cap n); p' = dest\<rbrakk> \<Longrightarrow> (untypedRange dest_cap \<subset> untypedRange src_cap \<longrightarrow> untypedRange dest_cap \<inter> usableUntypedRange scap = {}) \<and> (untypedRange src_cap \<subset> untypedRange dest_cap \<longrightarrow> untypedRange src_cap \<inter> usableUntypedRange dcap = {}) \<and> (untypedRange dest_cap = untypedRange src_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> src \<and> usableUntypedRange dcap = {} \<or> m \<turnstile> src \<rightarrow> dest \<and> usableUntypedRange scap = {})
 2. \<And>p' n c' n'. \<lbrakk>isUntypedCap dest_cap; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> n = n' \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dest_cap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dest_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p'); m dest = Some (CTE dest_cap n); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dcap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dcap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p')
 3. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p' n c' n'. \<lbrakk>isUntypedCap dest_cap; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> n = n' \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dest_cap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dest_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p'); m dest = Some (CTE dest_cap n); p' \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dcap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dcap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p')
 2. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p' n c' n'. \<lbrakk>isUntypedCap dest_cap; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> n = n' \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dest_cap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dest_cap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p'); m dest = Some (CTE dest_cap n); p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange dest_cap \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange dest_cap \<or> untypedRange dest_cap \<inter> untypedRange c' = {}) \<and> (untypedRange dest_cap \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> untypedRange dest_cap \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange dest_cap \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange dcap = {}) \<and> (untypedRange dest_cap = untypedRange c' \<longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange dcap = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> dest \<and> usableUntypedRange c' = {} \<or> src = p')
 2. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c. (\<exists>n. m (s_d_swap p src dest) = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')); p \<noteq> dest; p = src \<longrightarrow> m dest = Some (CTE dest_cap n) \<and> c = dcap; p \<noteq> src \<longrightarrow> m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p'); p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p'); p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src; p' = src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p')
 2. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p'); p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src; p' \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> m dest = Some (CTE dest_cap n') \<and> c' = dcap) \<and> (p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p'); p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src; p' \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n'); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p'); p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src; p' \<noteq> src\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; p' = dest \<longrightarrow> m src = Some (CTE src_cap n') \<and> c' = scap; p' \<noteq> dest \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n'); isUntypedCap c'; \<forall>c'. (\<exists>n'. m (s_d_swap p' src dest) = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p'); p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); p \<noteq> src; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest \<and> usableUntypedRange c = {} \<or> m \<turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal:
No subgoals!