theory CNodeInv_R

lemma irq_control_n: "irq_control n" using src dest dest_derived src_derived apply (clarsimp simp: irq_control_def) apply (frule revokable) apply (drule n_cap) apply (clarsimp split: if_split_asm) apply (clarsimp simp: weak_derived'_def) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (drule n_cap) apply (clarsimp split: if_split_asm) apply (drule (1) irq_controlD, rule irq_control) apply simp apply (drule (1) irq_controlD, rule irq_control) apply simp apply (clarsimp simp: weak_derived'_def) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (drule n_cap) apply (clarsimp split: if_split_asm) apply (drule (1) irq_controlD, rule irq_control) apply simp apply (drule (1) irq_controlD, rule irq_control) apply simp apply (clarsimp simp: weak_derived'_def) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (drule n_cap) apply (clarsimp split: if_split_asm) apply (drule (1) irq_controlD, rule irq_control) apply simp apply (drule (1) irq_controlD, rule irq_control) apply clarsimp apply (drule (1) irq_controlD, rule irq_control) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control n proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)
weak_derived' dest_cap dcap
weak_derived' src_cap scap

goal (1 subgoal):
 1. irq_control n proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; n p = Some (CTE capability.IRQControlCap na)\<rbrakk> \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; n p = Some (CTE capability.IRQControlCap na); if p = src then mdbRevocable na = mdbRevocable dest_node else if p = dest then mdbRevocable na = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then mdbRevocable na = mdbRevocable dest_node else if p = dest then mdbRevocable na = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable na = mdbRevocable node'; if p = src then capability.IRQControlCap = dcap else if p = dest then capability.IRQControlCap = scap else \<exists>node'. m p = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap capability.IRQControlCap; weak_derived' src_cap scap; mdbRevocable na = mdbRevocable dest_node; dcap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable dest_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = src)
 2. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable na = mdbRevocable dest_node; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap\<rbrakk> \<Longrightarrow> mdbRevocable dest_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = src)
 2. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable na = mdbRevocable dest_node; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable dest_node\<rbrakk> \<Longrightarrow> mdbRevocable dest_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = src)
 2. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>na p' n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable na; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable dest_node; n p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = src
 2. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>n p' n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable dest_node; if p' = src then capability.IRQControlCap = dcap else if p' = dest then capability.IRQControlCap = scap else \<exists>node'. m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> p' = src
 2. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; mdbRevocable dest_node; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 2. \<And>n p' node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable dest_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> False
 3. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 4. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; mdbRevocable dest_node; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap; dest = src\<rbrakk> \<Longrightarrow> False
 2. \<And>n p' node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable dest_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> False
 3. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 4. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>n p' node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable dest_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> False
 2. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>n p' node'. \<lbrakk>m src = Some (CTE src_cap src_node); mdbRevocable n; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable dest_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'); p' = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap capability.IRQControlCap; mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); mdbRevocable na = mdbRevocable src_node; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable src_node\<rbrakk> \<Longrightarrow> mdbRevocable src_node \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>na p' n'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); mdbRevocable na; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable src_node; n p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = dest
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>n p' n'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); mdbRevocable n; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable src_node; if p' = src then capability.IRQControlCap = dcap else if p' = dest then capability.IRQControlCap = scap else \<exists>node'. m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> p' = dest
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap; mdbRevocable src_node; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 2. \<And>n p' node'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); mdbRevocable n; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable src_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> False
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>m dest = Some (CTE capability.IRQControlCap dest_node); mdbRevocable n; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap; mdbRevocable src_node; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; dest = src\<rbrakk> \<Longrightarrow> False
 2. \<And>n p' node'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); mdbRevocable n; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable src_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> False
 3. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>n p' node'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); mdbRevocable n; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable src_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> False
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>n p' node'. \<lbrakk>m dest = Some (CTE dest_cap dest_node); mdbRevocable n; scap = capability.IRQControlCap; capMasterCap dest_cap = capMasterCap dcap; src_cap = capability.IRQControlCap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable src_node; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'); p' = src\<rbrakk> \<Longrightarrow> False
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); weak_derived' dest_cap dcap; weak_derived' src_cap scap; p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na = mdbRevocable node'; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na node' p' n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable na; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; n p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' n'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; if p' = src then capability.IRQControlCap = dcap else if p' = dest then capability.IRQControlCap = scap else \<exists>node'. m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (3 subgoals):
 1. \<And>p n node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.IRQControlCap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 2. \<And>p n node'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable node'; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 3. \<And>p n node' p' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (3 subgoals):
 1. \<And>p n node'. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; dcap = capability.IRQControlCap; dest_cap = capability.IRQControlCap; p = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>p n node'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable node'; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 3. \<And>p n node' p' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p n node'. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable node'; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 2. \<And>p n node' p' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p n node'. \<lbrakk>m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; mdbRevocable node'; scap = capability.IRQControlCap; src_cap = capability.IRQControlCap; p = src\<rbrakk> \<Longrightarrow> False
 2. \<And>p n node' p' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; mdbRevocable n; capMasterCap dest_cap = capMasterCap dcap; capMasterCap src_cap = capMasterCap scap; capBadge dest_cap = capBadge dcap; capBadge src_cap = capBadge scap; capASID dest_cap = capASID dcap; capASID src_cap = capASID scap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap; mdbRevocable node'; p' \<noteq> src; p' \<noteq> dest; m p' = Some (CTE capability.IRQControlCap node'a); p' = p\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal:
No subgoals!