theory CNodeInv_R

lemma caps_contained:
  "caps_contained' n" using valid apply (clarsimp simp: valid_mdb_ctes_def caps_contained'_def) apply (drule n_cap)+ apply (simp split: if_split_asm) apply (clarsimp dest!: capRange_untyped) apply fastforce apply fastforce apply fastforce apply fastforce apply (clarsimp dest!: capRange_untyped) apply fastforce apply fastforce apply fastforce done

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

goal (1 subgoal):
 1. caps_contained' n proof (prove)
goal (1 subgoal):
 1. \<And>p p' c na c' n' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE c na); n p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; if p = src then c = dcap else if p = dest then c = scap else \<exists>node'. m p = Some (CTE c node'); if p' = src then c' = dcap else if p' = dest then c' = scap else \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (9 subgoals):
 1. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange dest_cap \<noteq> {}; x \<in> capRange dest_cap; p = src; c = dcap; p' = src; c' = dcap\<rbrakk> \<Longrightarrow> x \<in> untypedRange dest_cap
 2. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange dest_cap \<noteq> {}; x \<in> capRange src_cap; p = src; c = dcap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange dest_cap
 3. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange dest_cap \<noteq> {}; x \<in> capRange c'; p = src; c = dcap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange dest_cap
 4. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange dest_cap; p = dest; c = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 5. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange dest_cap; p \<noteq> src; p \<noteq> dest; \<exists>node'. m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 6. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange src_cap; p = dest; c = scap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 7. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange c'; p = dest; c = scap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 8. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 9. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (8 subgoals):
 1. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange dest_cap \<noteq> {}; x \<in> capRange src_cap; p = src; c = dcap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange dest_cap
 2. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange dest_cap \<noteq> {}; x \<in> capRange c'; p = src; c = dcap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange dest_cap
 3. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange dest_cap; p = dest; c = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 4. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange dest_cap; p \<noteq> src; p \<noteq> dest; \<exists>node'. m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 5. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange src_cap; p = dest; c = scap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 6. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange c'; p = dest; c = scap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 7. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 8. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (7 subgoals):
 1. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange dest_cap \<noteq> {}; x \<in> capRange c'; p = src; c = dcap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange dest_cap
 2. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange dest_cap; p = dest; c = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 3. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange dest_cap; p \<noteq> src; p \<noteq> dest; \<exists>node'. m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange src_cap; p = dest; c = scap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 5. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange c'; p = dest; c = scap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 6. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 7. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (6 subgoals):
 1. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange dest_cap; p = dest; c = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 2. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange dest_cap; p \<noteq> src; p \<noteq> dest; \<exists>node'. m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange src_cap; p = dest; c = scap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 4. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange c'; p = dest; c = scap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 5. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 6. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (5 subgoals):
 1. \<And>p p' c c' x. \<lbrakk>p' = src; c' = dcap; valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap dest_cap; capRange dest_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange dest_cap; p \<noteq> src; p \<noteq> dest; \<exists>node'. m p = Some (CTE c node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange src_cap; p = dest; c = scap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 3. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange c'; p = dest; c = scap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 4. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 5. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (4 subgoals):
 1. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange src_cap; p = dest; c = scap; p' = dest; c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 2. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange c'; p = dest; c = scap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 3. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 4. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (3 subgoals):
 1. \<And>p p' c c' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; x \<in> capRange c'; p = dest; c = scap; p' \<noteq> src; p' \<noteq> dest; \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange src_cap
 2. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 3. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange src_cap; p \<noteq> src; p \<noteq> dest; p' = dest; m p = Some (CTE c node'); c' = scap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c
 2. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c' x node'. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<noteq> src; p \<noteq> dest; p' \<noteq> src; p' \<noteq> dest; m p = Some (CTE c node'); \<exists>node'. m p' = Some (CTE c' node')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal:
No subgoals!