theory Retype_IF

lemma machine_op_lift_ev':
  "equiv_valid_inv I A
     (K (\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and>
                   (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>))))
     (machine_op_lift mop)" unfolding machine_op_lift_def comp_def machine_rest_lift_def apply (rule gen_asm_ev) apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_bind) apply (rule gets_any_evrv) apply (rule_tac R'="\<top>\<top>" and Q="\<top>\<top>" and Q'="\<top>\<top>" in equiv_valid_2_bind_pre) apply (simp add: split_def) apply (rule modify_ev2) apply fastforce apply (rule select_f_any_ev2) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (K (\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)))) (machine_op_lift mop) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (K (\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)))) (do mr <- gets machine_state_rest;
(r, mr') <- select_f (ignore_failure mop mr);
modify (machine_state_rest_update (\<lambda>_. mr'));
return r
od) proof (prove)
goal (1 subgoal):
 1. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> equiv_valid_inv I A (\<lambda>_. True) (do mr <- gets machine_state_rest;
(r, mr') <- select_f (ignore_failure mop mr);
modify (machine_state_rest_update (\<lambda>_. mr'));
return r
od) proof (prove)
goal (1 subgoal):
 1. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> equiv_valid_rv_inv I A (=) (\<lambda>_. True) (do mr <- gets machine_state_rest;
(r, mr') <- select_f (ignore_failure mop mr);
modify (machine_state_rest_update (\<lambda>_. mr'))
od) proof (prove)
goal (3 subgoals):
 1. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> equiv_valid_rv_inv I A ?W2 (\<lambda>_. True) (gets machine_state_rest)
 2. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); ?W2 rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (=) (?Q2 rv) (?Q2 rv') (do (r, mr') <- select_f (ignore_failure mop rv);
modify (machine_state_rest_update (\<lambda>_. mr'))
od) (do (r, mr') <- select_f (ignore_failure mop rv');
modify (machine_state_rest_update (\<lambda>_. mr'))
od)
 3. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets machine_state_rest \<lbrace>?Q2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (=) (?Q2 rv) (?Q2 rv') (do (r, mr') <- select_f (ignore_failure mop rv);
modify (machine_state_rest_update (\<lambda>_. mr'))
od) (do (r, mr') <- select_f (ignore_failure mop rv');
modify (machine_state_rest_update (\<lambda>_. mr'))
od)
 2. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets machine_state_rest \<lbrace>?Q2\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (=) (\<lambda>_. True) (\<lambda>_. True) (case rva of (r, mr') \<Rightarrow> modify (machine_state_rest_update (\<lambda>_. mr'))) (case rv'a of (r, mr') \<Rightarrow> modify (machine_state_rest_update (\<lambda>_. mr')))
 2. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (\<lambda>_ _. True) (?P7 rv rv') (?P'7 rv rv') (select_f (ignore_failure mop rv)) (select_f (ignore_failure mop rv'))
 3. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S7 rv rv'\<rbrace> select_f (ignore_failure mop rv) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'7 rv rv'\<rbrace> select_f (ignore_failure mop rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv s\<rbrakk> \<Longrightarrow> ?P7 rv rv' s \<and> ?S7 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv' s\<rbrakk> \<Longrightarrow> ?P'7 rv rv' s \<and> ?S'7 rv rv' s
 7. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets machine_state_rest \<lbrace>?Q2\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rva rv'a. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> equiv_valid_2 I A A (=) (\<lambda>_. True) (\<lambda>_. True) (modify (machine_state_rest_update (\<lambda>_. snd rva))) (modify (machine_state_rest_update (\<lambda>_. snd rv'a)))
 2. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (\<lambda>_ _. True) (?P7 rv rv') (?P'7 rv rv') (select_f (ignore_failure mop rv)) (select_f (ignore_failure mop rv'))
 3. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S7 rv rv'\<rbrace> select_f (ignore_failure mop rv) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'7 rv rv'\<rbrace> select_f (ignore_failure mop rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv s\<rbrakk> \<Longrightarrow> ?P7 rv rv' s \<and> ?S7 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv' s\<rbrakk> \<Longrightarrow> ?P'7 rv rv' s \<and> ?S'7 rv rv' s
 7. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets machine_state_rest \<lbrace>?Q2\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rva rv'a s t. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); I s t; A s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> I (s\<lparr>machine_state_rest := snd rva\<rparr>) (t\<lparr>machine_state_rest := snd rv'a\<rparr>) \<and> A (s\<lparr>machine_state_rest := snd rva\<rparr>) (t\<lparr>machine_state_rest := snd rv'a\<rparr>)
 2. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (\<lambda>_ _. True) (?P7 rv rv') (?P'7 rv rv') (select_f (ignore_failure mop rv)) (select_f (ignore_failure mop rv'))
 3. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S7 rv rv'\<rbrace> select_f (ignore_failure mop rv) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'7 rv rv'\<rbrace> select_f (ignore_failure mop rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv s\<rbrakk> \<Longrightarrow> ?P7 rv rv' s \<and> ?S7 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv' s\<rbrakk> \<Longrightarrow> ?P'7 rv rv' s \<and> ?S'7 rv rv' s
 7. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets machine_state_rest \<lbrace>?Q2\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (\<lambda>_ _. True) (?P7 rv rv') (?P'7 rv rv') (select_f (ignore_failure mop rv)) (select_f (ignore_failure mop rv'))
 2. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S7 rv rv'\<rbrace> select_f (ignore_failure mop rv) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'7 rv rv'\<rbrace> select_f (ignore_failure mop rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv s\<rbrakk> \<Longrightarrow> ?P7 rv rv' s \<and> ?S7 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv' s\<rbrakk> \<Longrightarrow> ?P'7 rv rv' s \<and> ?S'7 rv rv' s
 6. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets machine_state_rest \<lbrace>?Q2\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S7 rv rv'\<rbrace> select_f (ignore_failure mop rv) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv rv'. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True\<rbrakk> \<Longrightarrow> \<lbrace>?S'7 rv rv'\<rbrace> select_f (ignore_failure mop rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv s\<rbrakk> \<Longrightarrow> True \<and> ?S7 rv rv' s
 4. \<And>rv rv' s. \<lbrakk>\<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)); True; ?Q2 rv' s\<rbrakk> \<Longrightarrow> True \<and> ?S'7 rv rv' s
 5. \<forall>s t x y. (I s t \<longrightarrow> I (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<and> (A s t \<longrightarrow> A (s\<lparr>machine_state_rest := x\<rparr>) (t\<lparr>machine_state_rest := y\<rparr>)) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets machine_state_rest \<lbrace>?Q2\<rbrace> proof (prove)
goal:
No subgoals!