theory Finalise_IF

lemma mapM_x_ev2_r_invisible:
  assumes domains_distinct:
    "pas_domains_distinct aag"
  assumes mam:
    "\<And>ptr. modifies_at_most aag (L ptr) \<top> ((f :: obj_ref \<Rightarrow> (unit, det_ext) s_monad) ptr)"
  assumes inv:
    "\<And>P. g \<lbrace>P\<rbrace>"
  shows
    "equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) \<top>
                   (K (\<forall>x. x \<in> set list \<longrightarrow>  labels_are_invisible aag l (L x))) g (mapM_x f list)" apply (induct list) apply (simp add: mapM_x_Nil) apply (rule ev2_inv[OF inv]) apply wp apply (simp add: mapM_x_Cons) apply (subst bind_return_unit2) apply (rule_tac R'="(=)" and P'="\<lambda> s. labels_are_invisible aag l (L a)" in equiv_valid_2_bind_pre) apply simp apply (rule gen_asm_ev2_r) apply (rule equiv_valid_2_guard_imp[OF ev2_invisible[OF domains_distinct]], assumption+) apply (rule_tac P="\<top>" in modifies_at_mostI) apply (wp | simp)+ apply (rule mam) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f list) proof (prove)
goal (2 subgoals):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f [])
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f (a # list)) proof (prove)
goal (2 subgoals):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. True) g (return ())
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f (a # list)) proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> return () \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) g (mapM_x f (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>b. \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) g (do y <- f a;
mapM_x f list
od) proof (prove)
goal (1 subgoal):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>b. \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (do _ <- return ();
g
od) (do y <- f a;
mapM_x f list
od) proof (prove)
goal (6 subgoals):
 1. \<And>a list rv rv'. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); rv = rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (?Q11 a list rv) (?Q'11 a list rv') g (mapM_x f list)
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P11 a list) (\<lambda>s. labels_are_invisible aag l (L a)) (return ()) (f a)
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S11 a list\<rbrace> return () \<lbrace>?Q11 a list\<rbrace>
 4. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S'11 a list\<rbrace> f a \<lbrace>?Q'11 a list\<rbrace>
 5. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); True\<rbrakk> \<Longrightarrow> ?P11 a list s \<and> ?S11 a list s
 6. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))\<rbrakk> \<Longrightarrow> labels_are_invisible aag l (L a) \<and> ?S'11 a list s proof (prove)
goal (5 subgoals):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P11 a list) (\<lambda>s. labels_are_invisible aag l (L a)) (return ()) (f a)
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S11 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S'11 a list\<rbrace> f a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)\<rbrace>
 4. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); True\<rbrakk> \<Longrightarrow> ?P11 a list s \<and> ?S11 a list s
 5. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))\<rbrakk> \<Longrightarrow> labels_are_invisible aag l (L a) \<and> ?S'11 a list s proof (prove)
goal (5 subgoals):
 1. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P11 a list) (\<lambda>_. True) (return ()) (f a)
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S11 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S'11 a list\<rbrace> f a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)\<rbrace>
 4. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); True\<rbrakk> \<Longrightarrow> ?P11 a list s \<and> ?S11 a list s
 5. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))\<rbrakk> \<Longrightarrow> labels_are_invisible aag l (L a) \<and> ?S'11 a list s proof (prove)
goal (9 subgoals):
 1. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q16 a list) (return ())
 2. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q'16 a list) (f a)
 3. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P16 a list s \<and> ?P'16 a list t \<longrightarrow> (\<forall>(rva, s')\<in>fst (return () s). \<forall>(rvb, t')\<in>fst (f a t). rva = rvb)
 4. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); ?P11 a list s\<rbrakk> \<Longrightarrow> (?P16 a list and ?Q16 a list) s
 5. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'16 a list and ?Q'16 a list) s
 6. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S11 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 7. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S'11 a list\<rbrace> f a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)\<rbrace>
 8. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); True\<rbrakk> \<Longrightarrow> ?P11 a list s \<and> ?S11 a list s
 9. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))\<rbrakk> \<Longrightarrow> labels_are_invisible aag l (L a) \<and> ?S'11 a list s proof (prove)
goal (9 subgoals):
 1. \<And>a list st. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and equiv_but_for_labels aag (L a) st\<rbrace> return () \<lbrace>\<lambda>_. equiv_but_for_labels aag (L a) st\<rbrace>
 2. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q'16 a list) (f a)
 3. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P16 a list s \<and> ?P'16 a list t \<longrightarrow> (\<forall>(rva, s')\<in>fst (return () s). \<forall>(rvb, t')\<in>fst (f a t). rva = rvb)
 4. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); ?P11 a list s\<rbrakk> \<Longrightarrow> (?P16 a list and (\<lambda>_. True)) s
 5. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'16 a list and ?Q'16 a list) s
 6. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S11 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 7. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S'11 a list\<rbrace> f a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)\<rbrace>
 8. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); True\<rbrakk> \<Longrightarrow> ?P11 a list s \<and> ?S11 a list s
 9. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))\<rbrakk> \<Longrightarrow> labels_are_invisible aag l (L a) \<and> ?S'11 a list s proof (prove)
goal (8 subgoals):
 1. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q'16 a list) (f a)
 2. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P16 a list s \<and> ?P'16 a list t \<longrightarrow> (\<forall>(rva, s')\<in>fst (return () s). \<forall>(rvb, t')\<in>fst (f a t). rva = rvb)
 3. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); ?P11 a list s\<rbrakk> \<Longrightarrow> (?P16 a list and (\<lambda>_. True)) s
 4. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'16 a list and ?Q'16 a list) s
 5. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S11 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 6. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S'11 a list\<rbrace> f a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)\<rbrace>
 7. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); True\<rbrakk> \<Longrightarrow> ?P11 a list s \<and> ?S11 a list s
 8. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))\<rbrakk> \<Longrightarrow> labels_are_invisible aag l (L a) \<and> ?S'11 a list s proof (prove)
goal (7 subgoals):
 1. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P16 a list s \<and> ?P'16 a list t \<longrightarrow> (\<forall>(rva, s')\<in>fst (return () s). \<forall>(rvb, t')\<in>fst (f a t). rva = rvb)
 2. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); ?P11 a list s\<rbrakk> \<Longrightarrow> (?P16 a list and (\<lambda>_. True)) s
 3. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'16 a list and (\<lambda>_. True)) s
 4. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S11 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list) \<Longrightarrow> \<lbrace>?S'11 a list\<rbrace> f a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)\<rbrace>
 6. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); True\<rbrakk> \<Longrightarrow> ?P11 a list s \<and> ?S11 a list s
 7. \<And>a list s. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) g (mapM_x f list); \<forall>x. (x = a \<longrightarrow> labels_are_invisible aag l (L a)) \<and> (x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))\<rbrakk> \<Longrightarrow> labels_are_invisible aag l (L a) \<and> ?S'11 a list s proof (prove)
goal:
No subgoals!