theory CNodeInv_R

lemma untyped_mdb_n:
  "untyped_mdb' n" using untyped_mdb apply (simp add: n_cap_eq untyped_mdb'_def descendants_of'_def parency) apply clarsimp apply (case_tac "p=dest") apply clarsimp apply (case_tac "p'=dest", simp) apply (case_tac "p'=src", simp) apply clarsimp apply clarsimp apply (case_tac "p'=dest") apply clarsimp apply (case_tac "p=src", simp) apply clarsimp apply clarsimp apply (case_tac "p=src") apply clarsimp apply (case_tac "p'=src",simp) apply clarsimp apply clarsimp apply (case_tac "p'=src",simp) apply clarsimp done

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

goal (1 subgoal):
 1. untyped_mdb' 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest) 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p = dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>p' 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>p' 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; p' \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>p' 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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' = dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>p c n 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; m src = Some (CTE src_cap n'); \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; 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> m \<turnstile> s_d_swap p src dest \<rightarrow> src
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>p c n 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; m src = Some (CTE src_cap n'); \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; 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> m \<turnstile> s_d_swap p src dest \<rightarrow> src
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); 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')); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> dest\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>p' 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap dest_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange dest_cap \<noteq> {}; m dest = Some (CTE dest_cap n); p' \<noteq> dest; p' = src \<longrightarrow> n = n' \<and> c' = dcap; p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n')\<rbrakk> \<Longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>p' 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap dest_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange dest_cap \<noteq> {}; m dest = Some (CTE dest_cap n); p' \<noteq> dest; p' = src \<longrightarrow> n = n' \<and> c' = dcap; p' \<noteq> src \<longrightarrow> m (s_d_swap p' src dest) = Some (CTE c' n'); p' \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> dest \<rightarrow> s_d_swap p' src dest
 2. \<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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 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> 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); 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> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest 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> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p \<noteq> dest; m (s_d_swap p src dest) = Some (CTE c n); 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; p' \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<rightarrow> s_d_swap p' src dest proof (prove)
goal:
No subgoals!