theory Retype_IF

lemma dmo_mapM_ev_pre:
  assumes reads_res: "\<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))"
  assumes invariant: "\<And>x. x \<in> set lst \<Longrightarrow> do_machine_op (m x) \<lbrace>I\<rbrace>"
  assumes inv_established: "\<And>s. P s \<Longrightarrow> I s"
  shows "equiv_valid_inv D A P (do_machine_op (mapM m lst))" using assms apply atomize apply (rule_tac Q=I in equiv_valid_guard_imp) apply (induct lst) apply (simp add: mapM_Nil return_ev_pre) apply (subst mapM_Cons) apply (simp add: dmo_bind_ev dmo_bind_ev') apply (rule bind_ev_pre[where P''="I"]) apply (rule bind_ev[OF return_ev]) apply fastforce apply (rule wp_post_taut) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (do_machine_op (mapM m lst)) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (m ?x))
?x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m ?x) \<lbrace>\<lambda>_. I\<rbrace>
P ?s \<Longrightarrow> I ?s

goal (1 subgoal):
 1. equiv_valid_inv D A P (do_machine_op (mapM m lst)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A P (do_machine_op (mapM m lst)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (mapM m lst))
 2. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x. x \<in> set [] \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set [] \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (mapM m []))
 2. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (mapM m (a # lst)))
 3. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (2 subgoals):
 1. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (mapM m (a # lst)))
 2. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (2 subgoals):
 1. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (do y <- m a;
ys <- mapM m lst;
return (y # ys)
od))
 2. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (2 subgoals):
 1. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do rv <- do_machine_op (m a);
rv' <- do_machine_op (mapM m lst);
return (rv # rv')
od)
 2. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (5 subgoals):
 1. \<And>a lst rv. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?Q6 a lst rv) (do rv' <- do_machine_op (mapM m lst);
return (rv # rv')
od)
 2. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (do_machine_op (m a))
 3. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>?Q6 a lst\<rbrace>
 4. \<And>a lst s. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 5. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (6 subgoals):
 1. \<And>a lst rv. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'11 a lst rv) (do_machine_op (mapM m lst))
 2. \<And>a lst rv. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>?P''11 a lst rv\<rbrace> do_machine_op (mapM m lst) \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (do_machine_op (m a))
 4. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>rv s. ?P'11 a lst rv s \<and> ?P''11 a lst rv s\<rbrace>
 5. \<And>a lst s. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 6. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (5 subgoals):
 1. \<And>a lst rv. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>?P''11 a lst rv\<rbrace> do_machine_op (mapM m lst) \<lbrace>\<lambda>rv' _. True\<rbrace>
 2. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (do_machine_op (m a))
 3. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>rv s. I s \<and> ?P''11 a lst rv s\<rbrace>
 4. \<And>a lst s. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 5. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (4 subgoals):
 1. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (do_machine_op (m a))
 2. \<And>a lst. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>rv s. I s \<and> True\<rbrace>
 3. \<And>a lst s. \<lbrakk>equiv_valid_inv D A I (do_machine_op (mapM m lst)); \<forall>x. (x = a \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m a))) \<and> (x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))); \<forall>x. (x = a \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m a) \<lbrace>\<lambda>_. I\<rbrace>) \<and> (x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>); \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 4. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (do_machine_op (m x)); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal:
No subgoals!