theory CNode_IF

lemma cap_swap_reads_respects:
  notes split_paired_All[simp del]
  shows "reads_respects aag l (K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)))
                        (cap_swap cap1 slot1 cap2 slot2)" unfolding cap_swap_def apply (subst gets_apply2) apply (simp add: bind_assoc[symmetric]) apply (fold update_cdt_def) apply (simp add: bind_assoc cap_swap_ext_def) apply (rule gen_asm_ev) apply (wp set_original_reads_respects update_cdt_reads_respects gets_apply_ev
            set_cap_reads_respects update_cdt_list_reads_respects
         | simp split del: if_split | fastforce simp: equiv_for_def split: option.splits)+ apply (intro impI conjI allI) apply ((fastforce simp: reads_equiv_def2 equiv_for_def
                        elim: states_equiv_forE_is_original_cap states_equiv_forE_cdt
                        dest: aag_can_read_self
                       split: option.splits)+)[2] apply (frule_tac x = slot1 in equiv_forD, elim conjE,drule aag_can_read_self,simp) apply (frule_tac x = slot2 in equiv_forD, elim conjE) apply (drule aag_can_read_self)+ apply clarsimp apply clarsimp apply (erule equiv_forE) apply (fastforce intro: equiv_forI) apply (fastforce simp: equiv_for_def dest: aag_can_read_self
                    elim: reads_equivE equiv_forE[where f="is_original_cap"] split: option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2))) (cap_swap cap1 slot1 cap2 slot2) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2))) (do set_cap cap2 slot1;
set_cap cap1 slot2;
slot1_p <- gets (\<lambda>s. cdt s slot1);
slot2_p <- gets (\<lambda>s. cdt s slot2);
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n);
set_cdt (cdt'(slot1 := cdt' slot2, slot2 := cdt' slot1));
do_extended_op (cap_swap_ext slot1 slot2 slot1_p slot2_p);
is_original <- gets is_original_cap;
set_original slot1 (is_original slot2);
set_original slot2 (is_original slot1)
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (fst slot1) \<and> is_subject aag (fst slot2))) (do set_cap cap2 slot1;
set_cap cap1 slot2;
slot1_p <- gets (\<lambda>s. cdt s slot1);
slot2_p <- gets (\<lambda>s. cdt s slot2);
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n);
set_cdt (cdt'(slot1 := cdt' slot2, slot2 := cdt' slot1));
do_extended_op (cap_swap_ext slot1 slot2 slot1_p slot2_p);
x <- gets_apply is_original_cap slot2;
y <- gets_apply is_original_cap slot1;
set_original slot1 x;
set_original slot2 y
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)) (do x <- do y <- do slot1_p <- do y <- do y <- set_cap cap2 slot1;
set_cap cap1 slot2
od;
gets (\<lambda>s. cdt s slot1)
od;
slot2_p <- gets (\<lambda>s. cdt s slot2);
y <- do cdt <- gets cdt;
set_cdt ((\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1))
od;
cap_swap_ext slot1 slot2 slot1_p slot2_p
od;
gets_apply is_original_cap slot2
od;
y <- gets_apply is_original_cap slot1;
ya <- set_original slot1 x;
set_original slot2 y
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)) (do x <- do y <- do slot1_p <- do y <- do y <- set_cap cap2 slot1;
set_cap cap1 slot2
od;
gets (\<lambda>s. cdt s slot1)
od;
slot2_p <- gets (\<lambda>s. cdt s slot2);
y <- update_cdt (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1));
cap_swap_ext slot1 slot2 slot1_p slot2_p
od;
gets_apply is_original_cap slot2
od;
y <- gets_apply is_original_cap slot1;
ya <- set_original slot1 x;
set_original slot2 y
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2)) (do x <- set_cap cap2 slot1;
x <- set_cap cap1 slot2;
x <- gets (\<lambda>s. cdt s slot1);
xa <- gets (\<lambda>s. cdt s slot2);
xb <- update_cdt (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1));
xb <- update_cdt_list (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1));
x <- update_cdt_list (\<lambda>list. case if xa = Some slot1 then Some slot2 else if xa = Some slot2 then Some slot1 else xa of None \<Rightarrow> case if x = Some slot1 then Some slot2 else if x = Some slot2 then Some slot1 else x of None \<Rightarrow> list | Some slot2_p \<Rightarrow> list(slot2_p := list_replace (list slot2_p) slot1 slot2) | Some slot1_p \<Rightarrow> case if x = Some slot1 then Some slot2 else if x = Some slot2 then Some slot1 else x of None \<Rightarrow> list(slot1_p := list_replace (list slot1_p) slot2 slot1) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2));
x <- gets_apply is_original_cap slot2;
y <- gets_apply is_original_cap slot1;
ya <- set_original slot1 x;
set_original slot2 y
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2) \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do x <- set_cap cap2 slot1;
x <- set_cap cap1 slot2;
x <- gets (\<lambda>s. cdt s slot1);
xa <- gets (\<lambda>s. cdt s slot2);
xb <- update_cdt (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1));
xb <- update_cdt_list (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1));
x <- update_cdt_list (\<lambda>list. case if xa = Some slot1 then Some slot2 else if xa = Some slot2 then Some slot1 else xa of None \<Rightarrow> case if x = Some slot1 then Some slot2 else if x = Some slot2 then Some slot1 else x of None \<Rightarrow> list | Some slot2_p \<Rightarrow> list(slot2_p := list_replace (list slot2_p) slot1 slot2) | Some slot1_p \<Rightarrow> case if x = Some slot1 then Some slot2 else if x = Some slot2 then Some slot1 else x of None \<Rightarrow> list(slot1_p := list_replace (list slot1_p) slot2 slot1) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2));
x <- gets_apply is_original_cap slot2;
y <- gets_apply is_original_cap slot1;
ya <- set_original slot1 x;
set_original slot2 y
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. is_subject aag (fst slot1) \<and> is_subject aag (fst slot2) \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cdt s slot1 = cdt t slot1) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cdt s slot2 = cdt t slot2) \<and> (\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv') \<and> (\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv') \<and> (\<forall>rv rv'. equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv' \<longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv') \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> is_original_cap s slot2 = is_original_cap t slot2) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> is_original_cap s slot1 = is_original_cap t slot1) proof (prove)
goal (7 subgoals):
 1. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> cdt sa slot1 = cdt t slot1
 2. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> cdt sa slot2 = cdt t slot2
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 4. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 5. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 6. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 7. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (5 subgoals):
 1. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 4. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 5. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (5 subgoals):
 1. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; id rv slot1 = id rv' slot1\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 4. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 5. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (6 subgoals):
 1. \<And>s rv rv'. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; id rv slot1 = id rv' slot1; is_subject aag (fst slot1); is_subject aag (fst slot2)\<rbrakk> \<Longrightarrow> ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) slot2
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; id rv slot1 = id rv' slot1; id rv slot2 = id rv' slot2\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 4. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 5. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 6. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (6 subgoals):
 1. \<And>s rv rv'. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; id rv slot1 = id rv' slot1; aag_can_read aag (fst slot1); aag_can_read aag (fst slot2)\<rbrakk> \<Longrightarrow> ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) slot2
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; id rv slot1 = id rv' slot1; id rv slot2 = id rv' slot2\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 4. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 5. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 6. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (5 subgoals):
 1. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; id rv slot1 = id rv' slot1; id rv slot2 = id rv' slot2\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 4. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 5. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; rv slot1 = rv' slot1; rv slot2 = rv' slot2; is_subject aag (fst slot1); is_subject aag (fst slot2)\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 4. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 5. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv slot1 = rv' slot1; rv slot2 = rv' slot2; is_subject aag (fst slot1); is_subject aag (fst slot2); \<And>x. ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) x \<Longrightarrow> id rv x = id rv' x\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>cdt. (\<lambda>n. if cdt n = Some slot1 then Some slot2 else if cdt n = Some slot2 then Some slot1 else cdt n)(slot1 := if cdt slot2 = Some slot1 then Some slot2 else if cdt slot2 = Some slot2 then Some slot1 else cdt slot2, slot2 := if cdt slot1 = Some slot1 then Some slot2 else if cdt slot1 = Some slot2 then Some slot1 else cdt slot1)) rv rv'
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 3. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 4. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 5. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal (4 subgoals):
 1. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)) rv rv'
 2. \<And>s rv rv'. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>a. a) rv rv'\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>a. aag_can_read aag (fst a) \<or> aag_can_affect aag l (fst a)) (\<lambda>list. case if cdt s slot2 = Some slot1 then Some slot2 else if cdt s slot2 = Some slot2 then Some slot1 else cdt s slot2 of None \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> list | Some slot2_p \<Rightarrow> \<lambda>a. if a = slot2_p then list_replace (list slot2_p) slot1 slot2 else list a | Some slot1_p \<Rightarrow> case if cdt s slot1 = Some slot1 then Some slot2 else if cdt s slot1 = Some slot2 then Some slot1 else cdt s slot1 of None \<Rightarrow> \<lambda>a. if a = slot1_p then list_replace (list slot1_p) slot2 slot1 else list a | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then list(slot1_p := list_swap (list slot1_p) slot1 slot2) else list(slot1_p := list_replace (list slot1_p) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2)) rv rv'
 3. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot2 = is_original_cap t slot2
 4. \<And>s sa t. \<lbrakk>is_subject aag (fst slot1) \<and> is_subject aag (fst slot2); reads_equiv aag sa t \<and> affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> is_original_cap sa slot1 = is_original_cap t slot1 proof (prove)
goal:
No subgoals!