theory CSpace_R

lemma irq_control_prev_update:
  "irq_control (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = irq_control m" apply (simp add: irq_control_def) apply (rule iffI) apply clarsimp apply (simp only: modify_map_if) apply (erule_tac x=p in allE) apply (simp (no_asm_use) split: if_split_asm) apply (case_tac "x=p") apply fastforce apply clarsimp apply (erule_tac x=p' in allE) apply simp apply (case_tac "x=p'") apply simp apply fastforce apply clarsimp apply (erule_tac x=p in allE) apply (simp add: modify_map_if split: if_split_asm) apply clarsimp apply (case_tac "x=p'") apply clarsimp apply clarsimp apply clarsimp apply (case_tac "x=p'") apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = irq_control m proof (prove)
goal (1 subgoal):
 1. (\<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)) = (\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)) proof (prove)
goal (2 subgoals):
 1. \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>\<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>\<forall>p n. (if x = p then \<exists>cap node. m x = Some (CTE cap node) \<and> cteMDBNode_update (mdbPrev_update f) (CTE cap node) = CTE capability.IRQControlCap n else \<exists>cap node. m p = Some (CTE cap node) \<and> CTE capability.IRQControlCap n = CTE cap node) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. if x = p' then \<exists>cap node. m x = Some (CTE cap node) \<and> cteMDBNode_update (mdbPrev_update f) (CTE cap node) = CTE capability.IRQControlCap n' else \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE capability.IRQControlCap n' = CTE cap node) \<longrightarrow> p' = p); m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); \<forall>n. (if x = p then \<exists>cap node. m x = Some (CTE cap node) \<and> cteMDBNode_update (mdbPrev_update f) (CTE cap node) = CTE capability.IRQControlCap n else \<exists>cap node. m p = Some (CTE cap node) \<and> CTE capability.IRQControlCap n = CTE cap node) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. if x = p' then \<exists>cap node. m x = Some (CTE cap node) \<and> cteMDBNode_update (mdbPrev_update f) (CTE cap node) = CTE capability.IRQControlCap n' else \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE capability.IRQControlCap n' = CTE cap node) \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>\<forall>n. (x = p \<longrightarrow> (\<forall>node. m p = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n) \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (p = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (p = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)) \<and> (m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> x = p \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (x = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (x = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)); m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p n. \<lbrakk>\<forall>n. (x = p \<longrightarrow> (\<forall>node. m p = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n) \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (p = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (p = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)) \<and> (m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> x = p \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (x = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (x = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)); m p = Some (CTE capability.IRQControlCap n); x = p\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 2. \<And>p n. \<lbrakk>\<forall>n. (x = p \<longrightarrow> (\<forall>node. m p = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n) \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (p = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (p = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)) \<and> (m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> x = p \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (x = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (x = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)); m p = Some (CTE capability.IRQControlCap n); x \<noteq> p\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 3. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>\<forall>n. (x = p \<longrightarrow> (\<forall>node. m p = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n) \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (p = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (p = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)) \<and> (m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> x = p \<or> mdbRevocable n \<and> (\<forall>p'. (\<forall>n'. (x = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (x = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p)); m p = Some (CTE capability.IRQControlCap n); x \<noteq> p\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); x \<noteq> p; mdbRevocable n; \<forall>p'. (\<forall>n'. (x = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (x = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p; m p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = p
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); x \<noteq> p; mdbRevocable n; m p' = Some (CTE capability.IRQControlCap n'); (\<forall>n'. (x = p' \<longrightarrow> (\<forall>node. m p' = Some (CTE capability.IRQControlCap node) \<longrightarrow> mdbPrev_update f node \<noteq> n')) \<and> (x = p' \<or> m p' \<noteq> Some (CTE capability.IRQControlCap n'))) \<or> p' = p\<rbrakk> \<Longrightarrow> p' = p
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); x \<noteq> p; mdbRevocable n; m p' = Some (CTE capability.IRQControlCap n'); (\<forall>n'a. (x = p' \<longrightarrow> mdbPrev_update f n' \<noteq> n'a) \<and> (x = p' \<or> n' \<noteq> n'a)) \<or> p' = p\<rbrakk> \<Longrightarrow> p' = p
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p n p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); x \<noteq> p; mdbRevocable n; m p' = Some (CTE capability.IRQControlCap n'); (\<forall>n'a. (x = p' \<longrightarrow> mdbPrev_update f n' \<noteq> n'a) \<and> (x = p' \<or> n' \<noteq> n'a)) \<or> p' = p; x = p'\<rbrakk> \<Longrightarrow> p' = p
 2. \<And>p n p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); x \<noteq> p; mdbRevocable n; m p' = Some (CTE capability.IRQControlCap n'); (\<forall>n'a. (x = p' \<longrightarrow> mdbPrev_update f n' \<noteq> n'a) \<and> (x = p' \<or> n' \<noteq> n'a)) \<or> p' = p; x \<noteq> p'\<rbrakk> \<Longrightarrow> p' = p
 3. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); x \<noteq> p; mdbRevocable n; m p' = Some (CTE capability.IRQControlCap n'); (\<forall>n'a. (x = p' \<longrightarrow> mdbPrev_update f n' \<noteq> n'a) \<and> (x = p' \<or> n' \<noteq> n'a)) \<or> p' = p; x \<noteq> p'\<rbrakk> \<Longrightarrow> p' = p
 2. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) \<Longrightarrow> \<forall>p n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE capability.IRQControlCap n); \<forall>n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p n. \<lbrakk>\<forall>n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); x = p; \<exists>node. m p = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. (p = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n')) \<and> (p \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p)
 2. \<And>p n. \<lbrakk>mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); x \<noteq> p; m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>n'. (x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n')) \<and> (x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>node p' n'. \<lbrakk>m x = Some (CTE capability.IRQControlCap node); mdbRevocable node; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = x; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = x
 2. \<And>p n. \<lbrakk>mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); x \<noteq> p; m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>n'. (x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n')) \<and> (x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p proof (prove)
goal (3 subgoals):
 1. \<And>node p' n'. \<lbrakk>m x = Some (CTE capability.IRQControlCap node); mdbRevocable node; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = x; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'); x = p'\<rbrakk> \<Longrightarrow> p' = x
 2. \<And>node p' n'. \<lbrakk>m x = Some (CTE capability.IRQControlCap node); mdbRevocable node; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = x; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'); x \<noteq> p'\<rbrakk> \<Longrightarrow> p' = x
 3. \<And>p n. \<lbrakk>mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); x \<noteq> p; m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>n'. (x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n')) \<and> (x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>node p' n'. \<lbrakk>m x = Some (CTE capability.IRQControlCap node); mdbRevocable node; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = x; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'); x \<noteq> p'\<rbrakk> \<Longrightarrow> p' = x
 2. \<And>p n. \<lbrakk>mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); x \<noteq> p; m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>n'. (x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n')) \<and> (x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); x \<noteq> p; m p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>n'. (x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n')) \<and> (x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'))) \<longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n p' n'. \<lbrakk>x \<noteq> p; m p = Some (CTE capability.IRQControlCap n); mdbRevocable n; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p n p' n'. \<lbrakk>x \<noteq> p; m p = Some (CTE capability.IRQControlCap n); mdbRevocable n; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'); x = p'\<rbrakk> \<Longrightarrow> p' = p
 2. \<And>p n p' n'. \<lbrakk>x \<noteq> p; m p = Some (CTE capability.IRQControlCap n); mdbRevocable n; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'); x \<noteq> p'\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n p' n'. \<lbrakk>x \<noteq> p; m p = Some (CTE capability.IRQControlCap n); mdbRevocable n; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p; x = p' \<longrightarrow> (\<exists>node. m p' = Some (CTE capability.IRQControlCap node) \<and> mdbPrev_update f node = n'); x \<noteq> p' \<longrightarrow> m p' = Some (CTE capability.IRQControlCap n'); x \<noteq> p'\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal:
No subgoals!