theory Finalise_IF

lemma mapM_x_ev2_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 mam':
    "\<And>ptr. modifies_at_most aag (L' ptr) \<top> ((f' :: obj_ref \<Rightarrow> (unit, det_ext) s_monad) ptr)"
  shows
    "equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=)
                   (K (\<forall>x. x \<in> set list' \<longrightarrow> (labels_are_invisible aag l (L' x))))
                   (K (\<forall>x. x \<in> set list \<longrightarrow> (labels_are_invisible aag l (L x))))
                   (mapM_x f' list') (mapM_x f list)" apply (induct list) apply (induct_tac list') apply (simp add: mapM_x_Nil) apply (blast intro: return_ev2) apply (simp add: mapM_x_Cons mapM_x_Nil) apply (subst bind_return_unit[where f="return ()"]) 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_l) apply (rule equiv_valid_2_guard_imp[OF ev2_invisible[OF domains_distinct]], assumption+) apply (rule mam') apply (rule_tac P="\<top>" in modifies_at_mostI) apply (wp | simp)+ 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) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) proof (prove)
goal (2 subgoals):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f [])
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' []) (mapM_x f [])
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list) (mapM_x f []) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' (a # list)) (mapM_x f [])
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>a b. True) (\<lambda>a. True) (return ())
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list) (mapM_x f []) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' (a # list)) (mapM_x f [])
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (2 subgoals):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list) (mapM_x f []) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set [] \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' (a # list)) (mapM_x f [])
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (2 subgoals):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. 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))) (\<lambda>a. True) (do y <- f' a;
mapM_x f' list
od) (return ())
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (2 subgoals):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. 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))) (\<lambda>a. True) (do y <- f' a;
mapM_x f' list
od) (do x <- return ();
return ()
od)
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (7 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); rv = rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (?Q12 a list rv) (?Q'12 a list rv') (mapM_x f' list) (return ())
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. labels_are_invisible aag l (L' a)) (?P'12 a list) (f' a) (return ())
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S12 a list\<rbrace> f' a \<lbrace>?Q12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S'12 a list\<rbrace> return () \<lbrace>?Q'12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); \<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> ?S12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); True\<rbrakk> \<Longrightarrow> ?P'12 a list s \<and> ?S'12 a list s
 7. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (6 subgoals):
 1. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. labels_are_invisible aag l (L' a)) (?P'12 a list) (f' a) (return ())
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S12 a list\<rbrace> f' a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S'12 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); \<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> ?S12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); True\<rbrakk> \<Longrightarrow> ?P'12 a list s \<and> ?S'12 a list s
 6. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (6 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (?P'12 a list) (f' a) (return ())
 2. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S12 a list\<rbrace> f' a \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S'12 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); \<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> ?S12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); True\<rbrakk> \<Longrightarrow> ?P'12 a list s \<and> ?S'12 a list s
 6. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) proof (prove)
goal (10 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L' a) (?Q17 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L' a) (?Q'17 a list) (return ())
 3. \<And>a list. \<lbrakk>equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P17 a list s \<and> ?P'17 a list t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f' a s). \<forall>(rvb, t')\<in>fst (return () 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a); True\<rbrakk> \<Longrightarrow> (?P17 a list and ?Q17 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a); ?P'12 a list s\<rbrakk> \<Longrightarrow> (?P'17 a list and ?Q'17 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S12 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. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S'12 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); \<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> ?S12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); True\<rbrakk> \<Longrightarrow> ?P'12 a list s \<and> ?S'12 a list s
 10. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L' a) (?Q'17 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P17 a list s \<and> ?P'17 a list t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f' a s). \<forall>(rvb, t')\<in>fst (return () 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a); True\<rbrakk> \<Longrightarrow> (?P17 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a); ?P'12 a list s\<rbrakk> \<Longrightarrow> (?P'17 a list and ?Q'17 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S12 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. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S'12 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); \<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> ?S12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); True\<rbrakk> \<Longrightarrow> ?P'12 a list s \<and> ?S'12 a list s
 9. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f (a # list)) 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P17 a list s \<and> ?P'17 a list t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f' a s). \<forall>(rvb, t')\<in>fst (return () 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a); True\<rbrakk> \<Longrightarrow> (?P17 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); labels_are_invisible aag l (L' a); ?P'12 a list s\<rbrakk> \<Longrightarrow> (?P'17 a list and (\<lambda>_. True)) s
 5. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S12 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. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()) \<Longrightarrow> \<lbrace>?S'12 a list\<rbrace> return () \<lbrace>\<lambda>a b. True\<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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); \<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> ?S12 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>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. True) (mapM_x f' list) (return ()); True\<rbrakk> \<Longrightarrow> ?P'12 a list s \<and> ?S'12 a list s
 9. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (K (\<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x))) (K (\<forall>x. x \<in> set (a # list) \<longrightarrow> labels_are_invisible aag l (L x))) (mapM_x f' list') (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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<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))) (mapM_x f' list') (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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<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))) (mapM_x f' list') (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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<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 ();
mapM_x f' list'
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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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) (?Q43 a list rv) (?Q'43 a list rv') (mapM_x f' list') (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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S43 a list\<rbrace> return () \<lbrace>?Q43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S'43 a list\<rbrace> f a \<lbrace>?Q'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrakk> \<Longrightarrow> ?P43 a list s \<and> ?S43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S43 a list\<rbrace> return () \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrakk> \<Longrightarrow> ?P43 a list s \<and> ?S43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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) (=) (?P43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S43 a list\<rbrace> return () \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 3. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrakk> \<Longrightarrow> ?P43 a list s \<and> ?S43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P48 a list s \<and> ?P'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); ?P43 a list s\<rbrakk> \<Longrightarrow> (?P48 a list and ?Q48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'48 a list and ?Q'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S43 a list\<rbrace> return () \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 7. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrakk> \<Longrightarrow> ?P43 a list s \<and> ?S43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P48 a list s \<and> ?P'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); ?P43 a list s\<rbrakk> \<Longrightarrow> (?P48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'48 a list and ?Q'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S43 a list\<rbrace> return () \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 7. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrakk> \<Longrightarrow> ?P43 a list s \<and> ?S43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> modifies_at_most aag (L a) (?Q'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P48 a list s \<and> ?P'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); ?P43 a list s\<rbrakk> \<Longrightarrow> (?P48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'48 a list and ?Q'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S43 a list\<rbrace> return () \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 6. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrakk> \<Longrightarrow> ?P43 a list s \<and> ?S43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a)\<rbrakk> \<Longrightarrow> \<forall>s t. ?P48 a list s \<and> ?P'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); ?P43 a list s\<rbrakk> \<Longrightarrow> (?P48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); labels_are_invisible aag l (L a); True\<rbrakk> \<Longrightarrow> (?P'48 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S43 a list\<rbrace> return () \<lbrace>\<lambda>a b. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrace>
 5. \<And>a list. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list) \<Longrightarrow> \<lbrace>?S'43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (mapM_x f list); \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)\<rbrakk> \<Longrightarrow> ?P43 a list s \<and> ?S43 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>a. \<forall>x. x \<in> set list' \<longrightarrow> labels_are_invisible aag l (L' x)) (\<lambda>a. \<forall>x. x \<in> set list \<longrightarrow> labels_are_invisible aag l (L x)) (mapM_x f' list') (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'43 a list s proof (prove)
goal:
No subgoals!