theory AutoCorres_C

lemma ccorres_to_corres_with_termination:
  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
  assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc)"
  assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)"
  assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'"
  assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')"
  assumes terminates:
    "\<And>s s'. \<lbrakk> cstate_relation s (globals s'); P s; \<not> snd (dspec_f s); G s' \<rbrakk> \<Longrightarrow>
             \<Gamma> \<turnstile> Call f_'proc \<down> Normal s'"
  shows "corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f" using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def rf_sr_def apply (clarsimp simp: corres_underlying_def ccorres_underlying_def) apply (rule conjI) apply (fastforce simp: unif_rrel_def intro: EHOther dest: in_AC_call_simpl) apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def) apply (cases check_term;
         clarsimp simp: select_f_def select_def snd_bind snd_assert get_def
                 split: sum.splits prod.splits) apply (erule impE, blast intro: terminates) apply (erule disjE) apply (monad_eq split: xstate.splits sum.splits) apply (drule EHOther, fastforce) apply blast apply (drule EHOther, fastforce) apply blast apply (monad_eq split: xstate.splits) apply (fastforce dest: EHAbrupt[OF _ EHEmpty]) apply (monad_eq split: xstate.splits sum.splits) apply (drule EHOther, fastforce) apply blast apply (drule EHOther, fastforce) apply blast apply (monad_eq split: xstate.splits) apply (fastforce dest: EHAbrupt[OF _ EHEmpty]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f proof (prove)
using this:
ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)
R ?r (ret_xf ?s') = R' ?r (ret_xf' ?s')
G ?s' \<Longrightarrow> ccorres_to_corres_pre Q (\<lambda>_. True) Q' ?s'

goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f proof (prove)
using this:
ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)
R ?r (ret_xf ?s') = R' ?r (ret_xf' ?s')
G ?s' \<Longrightarrow> Q (globals ?s') \<longrightarrow> True \<and> ?s' \<in> Q'

goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f (AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (dspec_f a). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r') \<and> \<not> snd (AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (dspec_f a). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'
 2. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> \<not> snd (AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> \<not> snd (AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a); snd ((do cur_gs <- get;
s <- select {s. globals s = cur_gs \<and> G s};
(rv, s') <- select_f ((do s <- get;
y <- assert (check_term \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
select (Collect (exec \<Gamma> (Call f_'proc) (Normal s))) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) s);
y <- put (globals s');
case rv of Inl x \<Rightarrow> fail | Inr x \<Rightarrow> return (Inr (ret_xf s'))
od) b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x. \<lbrakk>\<Gamma>\<turnstile>Call f_'proc \<down> Normal x \<longrightarrow> (\<exists>xa\<in>fst (return () x). \<forall>x2. xa = ((), x2) \<longrightarrow> (\<exists>xa. \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa \<and> snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x2))) \<or> (\<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))); \<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x\<rbrakk> \<Longrightarrow> False
 2. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; (\<exists>xa\<in>fst (return () x). \<forall>x2. xa = ((), x2) \<longrightarrow> (\<exists>xa. \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa \<and> snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x2))) \<or> (\<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x))))\<rbrakk> \<Longrightarrow> False
 2. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<exists>xa\<in>fst (return () x). \<forall>x2. xa = ((), x2) \<longrightarrow> (\<exists>xa. \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa \<and> snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x2))\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False
 3. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>a x x3. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Fault x3\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False
 4. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>a x x3. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<Gamma>\<turnstile>\<^sub>h \<langle>Call f_'proc # ?hs258 a x x3,x\<rangle> \<Rightarrow> (length (?hs258 a x x3), Fault x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False
 4. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False
 3. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<Gamma>\<turnstile>\<^sub>h \<langle>Call f_'proc # ?hs309 a x,x\<rangle> \<Rightarrow> (length (?hs309 a x), Stuck)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False
 3. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<exists>xa\<in>fst ((do s <- \<lambda>s. ({(s, s)}, False);
y <- assert (\<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x). \<forall>x1 x2. (xa = (x1, x2) \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (xa = (x1, x2) \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False
 2. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x x2. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); check_term; G x; \<Gamma>\<turnstile>Call f_'proc \<down> Normal x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> False
 2. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x x3. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Fault x3\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x x3. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile>\<^sub>h \<langle>Call f_'proc # ?hs536 a x x3,x\<rangle> \<Rightarrow> (length (?hs536 a x x3), Fault x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile>\<^sub>h \<langle>Call f_'proc # ?hs587 a x,x\<rangle> \<Rightarrow> (length (?hs587 a x), Stuck)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a x x2. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); \<not> check_term; G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!