theory Syscall_IF

lemma syscall_requiv_f_g:
  "\<lbrakk> reads_respects_f_g aag l P m_fault;
     \<And>v. reads_respects_f_g aag l (R' v) (h_error v);
     \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v);
     \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v);
     \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v);
     \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>;
     \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace> \<rbrakk>
     \<Longrightarrow> reads_respects_f_g aag l P (syscall m_fault h_fault m_error h_error m_finalise)" apply (rule syscall_reads_respects_f_g[where Q''="\<lambda>rv. Q'' rv and Q''' rv"]) apply (unfold validE_def) apply (assumption)+ apply (rule equiv_valid_guard_imp, assumption, simp) apply assumption+ apply (rule hoare_strengthen_post) apply assumption apply (simp split: sum.splits) apply (rule hoare_strengthen_post, rule hoare_pre) apply assumption apply simp apply (simp split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l P (syscall m_fault h_fault m_error h_error m_finalise) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l P m_fault
 2. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (Q'' v and Q''' v) (m_error v)
 3. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?Q' v) (h_fault v)
 4. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R'' v) (m_finalise v)
 5. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R' v) (h_error v)
 6. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m_fault \<lbrace>case_sum ?Q' (\<lambda>rv. Q'' rv and Q''' rv)\<rbrace>
 7. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>R''\<rbrace>, \<lbrace>R'\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>rv. Q'' rv and Q''' rv\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum ?R' ?R''\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l P m_fault
 2. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (Q'' v and Q''' v) (m_error v)
 3. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?Q' v) (h_fault v)
 4. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R'' v) (m_finalise v)
 5. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R' v) (h_error v)
 6. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m_fault \<lbrace>case_sum ?Q' (\<lambda>rv. Q'' rv and Q''' rv)\<rbrace>
 7. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum ?R' ?R''\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (Q'' v and Q''' v) (m_error v)
 2. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?Q' v) (h_fault v)
 3. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R'' v) (m_finalise v)
 4. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R' v) (h_error v)
 5. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m_fault \<lbrace>case_sum ?Q' (\<lambda>rv. Q'' rv and Q''' rv)\<rbrace>
 6. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum ?R' ?R''\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?Q' v) (h_fault v)
 2. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R'' v) (m_finalise v)
 3. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (?R' v) (h_error v)
 4. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m_fault \<lbrace>case_sum ?Q' (\<lambda>rv. Q'' rv and Q''' rv)\<rbrace>
 5. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum ?R' ?R''\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m_fault \<lbrace>case_sum Q' (\<lambda>rv. Q'' rv and Q''' rv)\<rbrace>
 2. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum R' R''\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m_fault \<lbrace>?Q19\<rbrace>
 2. \<And>rv s. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>; ?Q19 rv s\<rbrakk> \<Longrightarrow> (case rv of Inl v \<Rightarrow> Q' v | Inr rv \<Rightarrow> Q'' rv and Q''' rv) s
 3. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum R' R''\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>; case rv of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrakk> \<Longrightarrow> (case rv of Inl v \<Rightarrow> Q' v | Inr rv \<Rightarrow> Q'' rv and Q''' rv) s
 2. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum R' R''\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'' v and Q''' v\<rbrace> m_error v \<lbrace>case_sum R' R''\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>v. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q54 v\<rbrace> m_error v \<lbrace>?Q51 v\<rbrace>
 2. \<And>v s. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>; (Q'' v and Q''' v) s\<rbrakk> \<Longrightarrow> ?Q54 v s
 3. \<And>v rv s. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>; ?Q51 v rv s\<rbrakk> \<Longrightarrow> (case rv of Inl v \<Rightarrow> R' v | Inr v \<Rightarrow> R'' v) s proof (prove)
goal (2 subgoals):
 1. \<And>v s. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>; (Q'' v and Q''' v) s\<rbrakk> \<Longrightarrow> Q''' v s
 2. \<And>v rv s. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>; case rv of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrakk> \<Longrightarrow> (case rv of Inl v \<Rightarrow> R' v | Inr v \<Rightarrow> R'' v) s proof (prove)
goal (1 subgoal):
 1. \<And>v rv s. \<lbrakk>reads_respects_f_g aag l P m_fault; \<And>v. reads_respects_f_g aag l (R' v) (h_error v); \<And>v. reads_respects_f_g aag l (R'' v) (m_finalise v); \<And>v. reads_respects_f_g aag l (Q'' v) (m_error v); \<And>v. reads_respects_f_g aag l (Q' v) (h_fault v); \<And>v. \<lbrace>Q''' v\<rbrace> m_error v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrace>; \<lbrace>P\<rbrace> m_fault \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> (Q'' r and Q''' r) s\<rbrace>; case rv of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> R'' r s\<rbrakk> \<Longrightarrow> (case rv of Inl v \<Rightarrow> R' v | Inr v \<Rightarrow> R'' v) s proof (prove)
goal:
No subgoals!