theory CNodeInv_AI

lemma untyped_inc_n:
  assumes untyped_eq:"(is_untyped_cap cap \<Longrightarrow> scap = cap)" "(is_untyped_cap cap' \<Longrightarrow> dcap = cap')"
  shows "untyped_inc n cs'" proof - from valid_mdb have "untyped_inc m cs" by (simp add: cs_def m valid_mdb_def2) thus ?thesis using cap cap' apply (simp add: untyped_inc_def cs'_def descendants_of_def parency s_d_swap_def
                del: split_paired_All) apply (intro allI) apply (intro conjI) apply (intro impI allI) apply (intro conjI) apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (clarsimp simp:untyped_eq) apply (intro impI allI) apply (drule_tac x = p' in spec) apply (drule_tac x = dest in spec) apply (clarsimp simp:untyped_eq) apply (intro impI) apply (intro conjI) apply (intro impI allI) apply (drule_tac x = src in spec) apply (intro conjI) apply (drule_tac x = dest in spec) apply (clarsimp simp:untyped_eq) apply (drule_tac x = p' in spec) apply (clarsimp simp:untyped_eq) apply (intro impI allI) apply (intro conjI) apply (drule_tac x = dest in spec) apply (drule_tac x = p in spec) apply (clarsimp simp:untyped_eq) apply (drule_tac x = src in spec) apply (drule_tac x = p in spec) apply (clarsimp simp:untyped_eq) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc n cs' proof (state)
goal (1 subgoal):
 1. untyped_inc n cs' proof (chain)
picking this:
valid_mdb s proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. untyped_inc m cs proof (state)
this:
untyped_inc m cs

goal (1 subgoal):
 1. untyped_inc n cs' proof (prove)
using this:
untyped_inc m cs

goal (1 subgoal):
 1. untyped_inc n cs' proof (prove)
using this:
untyped_inc m cs
cs src = Some cap
cs dest = Some cap'

goal (1 subgoal):
 1. untyped_inc n cs' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> \<forall>p. (p = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (\<forall>p'. p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range cap \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {})) \<and> (p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))))) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (\<forall>p'. p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range cap \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {})) \<and> (p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))))) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (\<forall>p'. p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range cap \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {})) \<and> (p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {}))))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range cap \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {})) \<and> (p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {})))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src\<rbrakk> \<Longrightarrow> p' = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range cap \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {})
 2. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {}))
 3. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src; \<forall>p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p'))\<rbrakk> \<Longrightarrow> p' = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range cap \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {})
 2. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {}))
 3. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src; \<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p'))\<rbrakk> \<Longrightarrow> p' = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range cap \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {})
 2. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {}))
 3. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {}))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src; p' \<noteq> dest; cs p' = Some c'; is_untyped_cap c'\<rbrakk> \<Longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {})
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src; p' \<noteq> dest; cs p' = Some c'; is_untyped_cap c'; \<forall>p'a c. cs p' = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p'a = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p'a \<rightarrow> p' \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p' \<rightarrow> p'a \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p'a \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p'a \<rightarrow> p' \<and> usable_untyped_range c' = {} \<or> p' = p'a))\<rbrakk> \<Longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {})
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p = src; is_untyped_cap cap'; p' \<noteq> src; p' \<noteq> dest; cs p' = Some c'; is_untyped_cap c'; \<forall>c. cs p' = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs dest = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p' \<rightarrow> dest \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range c' = {} \<or> p' = dest))\<rbrakk> \<Longrightarrow> (untyped_range c' \<subset> untyped_range cap' \<longrightarrow> untyped_range c' \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range dcap = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {})
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))))) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap\<rbrakk> \<Longrightarrow> (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {})))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> (p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {})))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})
 2. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))
 3. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap; \<forall>c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs dest = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = dest))\<rbrakk> \<Longrightarrow> p' = src \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range cap \<subset> untyped_range cap' \<longrightarrow> untyped_range cap \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range cap' \<subset> untyped_range cap \<longrightarrow> untyped_range cap' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range cap' \<longrightarrow> m \<Turnstile> src \<rightarrow> dest \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> dest \<rightarrow> src \<and> usable_untyped_range dcap = {})
 2. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))
 3. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p = dest; is_untyped_cap cap; \<forall>c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> untyped_range c' \<inter> usable_untyped_range scap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range scap = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {}))
 2. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})))) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))) \<and> (p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {}))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))
 2. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest; \<forall>p' c. cs dest = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> dest \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> dest \<and> usable_untyped_range c' = {} \<or> dest = p'))\<rbrakk> \<Longrightarrow> p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))
 2. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest; \<forall>c. cs dest = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> dest \<rightarrow> p \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c' = {} \<or> dest = p))\<rbrakk> \<Longrightarrow> p' = src \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap' \<longrightarrow> (untyped_range c \<subset> untyped_range cap' \<longrightarrow> untyped_range c \<inter> usable_untyped_range dcap = {}) \<and> (untyped_range c = untyped_range cap' \<longrightarrow> m \<Turnstile> p \<rightarrow> dest \<and> usable_untyped_range c = {} \<or> m \<Turnstile> dest \<rightarrow> p \<and> usable_untyped_range dcap = {}))
 2. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>\<forall>p p' c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> p \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> p \<and> usable_untyped_range c' = {} \<or> p = p')); cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest; \<forall>p' c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p' \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p' \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p' \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p'))\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; p \<noteq> src; p \<noteq> dest; \<forall>c. cs src = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. cs p = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> m \<Turnstile> src \<rightarrow> p \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range c = {} \<or> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c' = {} \<or> src = p))\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> p' = dest \<longrightarrow> (\<forall>c. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subset> untyped_range cap \<longrightarrow> untyped_range c \<inter> usable_untyped_range scap = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> m \<Turnstile> p \<rightarrow> src \<and> usable_untyped_range c = {} \<or> m \<Turnstile> src \<rightarrow> p \<and> usable_untyped_range scap = {})) proof (prove)
goal:
No subgoals! proof (state)
this:
untyped_inc n cs'

goal:
No subgoals!