theory CNodeInv_AI

lemma mdb_cte_n:
  "mdb_cte_at (\<lambda>p. \<exists>c. cs' p = Some c \<and> cap.NullCap \<noteq> c) n" proof - from valid_mdb have "mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> cap.NullCap \<noteq> c) m" by (simp add: cs_def m valid_mdb_def2) thus ?thesis using cap cap' sder dder apply (clarsimp simp add: mdb_cte_at_def) apply (cases src, cases dest) apply (simp add: n_def n'_def cs'_def split: if_split_asm) apply fastforce apply fastforce apply fastforce apply fastforce apply fastforce apply fastforce apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (\<lambda>p. \<exists>c. cs' p = Some c \<and> NullCap \<noteq> c) n proof (state)
goal (1 subgoal):
 1. mdb_cte_at (\<lambda>p. \<exists>c. cs' p = Some c \<and> NullCap \<noteq> c) n proof (chain)
picking this:
valid_mdb s proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m proof (state)
this:
mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m

goal (1 subgoal):
 1. mdb_cte_at (\<lambda>p. \<exists>c. cs' p = Some c \<and> NullCap \<noteq> c) n proof (prove)
using this:
mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m

goal (1 subgoal):
 1. mdb_cte_at (\<lambda>p. \<exists>c. cs' p = Some c \<and> NullCap \<noteq> c) n proof (prove)
using this:
mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m
cs src = Some cap
cs dest = Some cap'
weak_derived scap cap
weak_derived dcap cap'

goal (1 subgoal):
 1. mdb_cte_at (\<lambda>p. \<exists>c. cs' p = Some c \<and> NullCap \<noteq> c) n proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; n (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (\<exists>c. cs' (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs' (aa, ba) = Some c \<and> NullCap \<noteq> c) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>\<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; n (aa, ba) = Some (a, b); src = (ab, bb); dest = (ac, bc)\<rbrakk> \<Longrightarrow> (\<exists>c. cs' (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs' (aa, ba) = Some c \<and> NullCap \<noteq> c) proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba ab ac bc. \<lbrakk>src = (a, b); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (a, b) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac; ba = bc; m (a, b) = Some (ac, bc); ab = a\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> (ac = a \<and> bc = b \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap) \<and> ((ac = a \<longrightarrow> bc \<noteq> b) \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap))
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac; ba = bc; a = ac \<longrightarrow> b \<noteq> bc; m (ab, bb) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap))) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> NullCap \<noteq> scap)) \<and> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> NullCap \<noteq> scap))
 3. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; ab = a \<longrightarrow> bb \<noteq> b; aa = ab; ba = bb; m (a, b) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; ab = ac \<longrightarrow> bb \<noteq> bc; aa = ab; ba = bb; a = ab \<longrightarrow> b \<noteq> bb; m (ac, bc) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> cap') \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (a = ac \<and> b = bc \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap) \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 5. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = a \<longrightarrow> ba \<noteq> b; aa = ab \<longrightarrow> ba \<noteq> bb; m (aa, ba) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = a \<longrightarrow> bb \<noteq> b) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = a \<and> ba = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)
 6. \<And>a b aa ba ab ac bc. \<lbrakk>src = (a, b); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (a, b) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = a \<longrightarrow> ba \<noteq> b; ac = a \<longrightarrow> bc \<noteq> b; m (aa, ba) = Some (ac, bc); ab = a\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = a \<and> ba = b \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 7. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = ab \<longrightarrow> ba \<noteq> bb; a = ab \<longrightarrow> b \<noteq> bb; a = ac \<longrightarrow> b \<noteq> bc; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)) \<and> (a = ac \<and> b = bc \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac; ba = bc; a = ac \<longrightarrow> b \<noteq> bc; m (ab, bb) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap))) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> NullCap \<noteq> scap)) \<and> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> NullCap \<noteq> scap))
 2. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; ab = a \<longrightarrow> bb \<noteq> b; aa = ab; ba = bb; m (a, b) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; ab = ac \<longrightarrow> bb \<noteq> bc; aa = ab; ba = bb; a = ab \<longrightarrow> b \<noteq> bb; m (ac, bc) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> cap') \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (a = ac \<and> b = bc \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap) \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 4. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = a \<longrightarrow> ba \<noteq> b; aa = ab \<longrightarrow> ba \<noteq> bb; m (aa, ba) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = a \<longrightarrow> bb \<noteq> b) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = a \<and> ba = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)
 5. \<And>a b aa ba ab ac bc. \<lbrakk>src = (a, b); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (a, b) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = a \<longrightarrow> ba \<noteq> b; ac = a \<longrightarrow> bc \<noteq> b; m (aa, ba) = Some (ac, bc); ab = a\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = a \<and> ba = b \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 6. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = ab \<longrightarrow> ba \<noteq> bb; a = ab \<longrightarrow> b \<noteq> bb; a = ac \<longrightarrow> b \<noteq> bc; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)) \<and> (a = ac \<and> b = bc \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; ab = a \<longrightarrow> bb \<noteq> b; aa = ab; ba = bb; m (a, b) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; ab = ac \<longrightarrow> bb \<noteq> bc; aa = ab; ba = bb; a = ab \<longrightarrow> b \<noteq> bb; m (ac, bc) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> cap') \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (a = ac \<and> b = bc \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap) \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 3. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = a \<longrightarrow> ba \<noteq> b; aa = ab \<longrightarrow> ba \<noteq> bb; m (aa, ba) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = a \<longrightarrow> bb \<noteq> b) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = a \<and> ba = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)
 4. \<And>a b aa ba ab ac bc. \<lbrakk>src = (a, b); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (a, b) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = a \<longrightarrow> ba \<noteq> b; ac = a \<longrightarrow> bc \<noteq> b; m (aa, ba) = Some (ac, bc); ab = a\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = a \<and> ba = b \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 5. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = ab \<longrightarrow> ba \<noteq> bb; a = ab \<longrightarrow> b \<noteq> bb; a = ac \<longrightarrow> b \<noteq> bc; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)) \<and> (a = ac \<and> b = bc \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; ab = ac \<longrightarrow> bb \<noteq> bc; aa = ab; ba = bb; a = ab \<longrightarrow> b \<noteq> bb; m (ac, bc) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> cap') \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (a = ac \<and> b = bc \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap) \<and> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 2. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = a \<longrightarrow> ba \<noteq> b; aa = ab \<longrightarrow> ba \<noteq> bb; m (aa, ba) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = a \<longrightarrow> bb \<noteq> b) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = a \<and> ba = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)
 3. \<And>a b aa ba ab ac bc. \<lbrakk>src = (a, b); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (a, b) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = a \<longrightarrow> ba \<noteq> b; ac = a \<longrightarrow> bc \<noteq> b; m (aa, ba) = Some (ac, bc); ab = a\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = a \<and> ba = b \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = ab \<longrightarrow> ba \<noteq> bb; a = ab \<longrightarrow> b \<noteq> bb; a = ac \<longrightarrow> b \<noteq> bc; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)) \<and> (a = ac \<and> b = bc \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb ac. \<lbrakk>src = (ab, bb); dest = (a, b); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (a, b) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = a \<longrightarrow> ba \<noteq> b; aa = ab \<longrightarrow> ba \<noteq> bb; m (aa, ba) = Some (ab, bb); ac = a\<rbrakk> \<Longrightarrow> (a = ab \<and> b = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = a \<and> bb = b \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = a \<longrightarrow> bb \<noteq> b) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = a \<and> ba = b \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)
 2. \<And>a b aa ba ab ac bc. \<lbrakk>src = (a, b); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (a, b) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = a \<longrightarrow> ba \<noteq> b; ac = a \<longrightarrow> bc \<noteq> b; m (aa, ba) = Some (ac, bc); ab = a\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = a \<and> ba = b \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = ab \<longrightarrow> ba \<noteq> bb; a = ab \<longrightarrow> b \<noteq> bb; a = ac \<longrightarrow> b \<noteq> bc; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)) \<and> (a = ac \<and> b = bc \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab ac bc. \<lbrakk>src = (a, b); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (a, b) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = a \<longrightarrow> ba \<noteq> b; ac = a \<longrightarrow> bc \<noteq> b; m (aa, ba) = Some (ac, bc); ab = a\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((a = ac \<longrightarrow> b \<noteq> bc) \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = a \<and> ba = b \<longrightarrow> (a = ac \<and> b = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = ab \<longrightarrow> ba \<noteq> bb; a = ab \<longrightarrow> b \<noteq> bb; a = ac \<longrightarrow> b \<noteq> bc; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)) \<and> (a = ac \<and> b = bc \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>src = (ab, bb); dest = (ac, bc); \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); cs (ab, bb) = Some cap; cs (ac, bc) = Some cap'; weak_derived scap cap; weak_derived dcap cap'; aa = ac \<longrightarrow> ba \<noteq> bc; aa = ab \<longrightarrow> ba \<noteq> bb; a = ab \<longrightarrow> b \<noteq> bb; a = ac \<longrightarrow> b \<noteq> bc; m (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> (a = ac \<and> b = bc \<longrightarrow> (ac = ab \<and> bc = bb \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ac = ab \<longrightarrow> bc \<noteq> bb) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap)) \<and> (a = ab \<and> b = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> dcap \<and> NullCap \<noteq> scap) \<and> NullCap \<noteq> dcap)) \<and> (a = ac \<and> b = bc \<longrightarrow> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> scap \<and> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) \<and> NullCap \<noteq> scap) \<and> (aa = ab \<and> ba = bb \<longrightarrow> (ab = ac \<and> bb = bc \<longrightarrow> NullCap \<noteq> scap) \<and> ((ab = ac \<longrightarrow> bb \<noteq> bc) \<longrightarrow> NullCap \<noteq> dcap)) \<and> (aa = ac \<and> ba = bc \<longrightarrow> NullCap \<noteq> scap) proof (prove)
goal:
No subgoals! proof (state)
this:
mdb_cte_at (\<lambda>p. \<exists>c. cs' p = Some c \<and> NullCap \<noteq> c) n

goal:
No subgoals!